1 files changed, 16 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 581ee4d7..6c974948 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -397,6 +397,22 @@ function pfl(s) {
     er("Can't parse float: " + s);
 }
 
+function pio(s) {
+  var r = parseInt(s);
+  if (r.toString() == s)
+    return r;
+  else
+    return null;
+}
+
+function pflo(s) {
+  var r = parseFloat(s);
+  if (r.toString() == s)
+    return r;
+  else
+    return null;
+}
+
 function uf(s) {
   return escape(s).replace(new RegExp ("/", "g"), "%2F");
 }