comparison lib/js/urweb.js @ 1621:62d6d452c2b8

Change client-side int parsing to match server-side, in ignoring initial zeroes
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Dec 2011 10:07:50 -0500
parents 43f22a8f76cc
children a20daedfd1d0
comparison
equal deleted inserted replaced
1620:43f22a8f76cc 1621:62d6d452c2b8
942 } 942 }
943 function ssub(s, start, len) { 943 function ssub(s, start, len) {
944 return s.substring(start, start+len); 944 return s.substring(start, start+len);
945 } 945 }
946 946
947 function trimZeroes(s) {
948 for (var i = 0; i < s.length; ++i)
949 if (s[i] != '0') {
950 if (i > 0)
951 return s.substring(i);
952 else
953 return s;
954 }
955
956 if (s == "0")
957 return s;
958 else
959 er("Can't parse int: " + s);
960 }
961
947 function pi(s) { 962 function pi(s) {
963 s = trimZeroes(s);
948 var r = parseInt(s); 964 var r = parseInt(s);
949 if (r.toString() == s) 965 if (r.toString() == s)
950 return r; 966 return r;
951 else 967 else
952 er("Can't parse int: " + s); 968 er("Can't parse int: " + s);
959 else 975 else
960 er("Can't parse float: " + s); 976 er("Can't parse float: " + s);
961 } 977 }
962 978
963 function pio(s) { 979 function pio(s) {
980 s = trimZeroes(s);
964 var r = parseInt(s); 981 var r = parseInt(s);
965 if (r.toString() == s) 982 if (r.toString() == s)
966 return r; 983 return r;
967 else 984 else
968 return null; 985 return null;