diff 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
line wrap: on
line diff
--- a/lib/js/urweb.js	Sat Dec 03 10:00:10 2011 -0500
+++ b/lib/js/urweb.js	Sat Dec 03 10:07:50 2011 -0500
@@ -944,7 +944,23 @@
     return s.substring(start, start+len);
 }
 
+function trimZeroes(s) {
+    for (var i = 0; i < s.length; ++i)
+        if (s[i] != '0') {
+            if (i > 0)
+                return s.substring(i);
+            else
+                return s;
+        }
+
+    if (s == "0")
+        return s;
+    else
+        er("Can't parse int: " + s);
+}
+
 function pi(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;
@@ -961,6 +977,7 @@
 }
 
 function pio(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;