From f944c1f6dd0f0161b7e8aa5d6f8dbc721164d462 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 3 Dec 2011 10:07:50 -0500
Subject: Change client-side int parsing to match server-side, in ignoring
 initial zeroes

---
 lib/js/urweb.js | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'lib/js')

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 015befa6..2dff3df6 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -944,7 +944,23 @@ function ssub(s, start, len) {
     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 pfl(s) {
 }
 
 function pio(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;
-- 
cgit v1.2.3