diff lib/js/urweb.js @ 838:5154a047c6bc

Lexing some more string escape sequences; JS versions of number read; fix problem with signature unification; escape < more often in Jscomp
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Jun 2009 19:28:25 -0400
parents b0a85cbefed2
children 44c2c089ca15
line wrap: on
line diff
--- a/lib/js/urweb.js	Tue Jun 02 15:43:18 2009 -0400
+++ b/lib/js/urweb.js	Tue Jun 02 19:28:25 2009 -0400
@@ -397,6 +397,22 @@
     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");
 }