diff lib/js/urweb.js @ 649:96ebc6bdb5a0

Batch example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 15:17:23 -0400
parents fb2a0e76dcef
children a93d5324f400
line wrap: on
line diff
--- a/lib/js/urweb.js	Tue Mar 10 13:57:09 2009 -0400
+++ b/lib/js/urweb.js	Tue Mar 10 15:17:23 2009 -0400
@@ -99,7 +99,26 @@
 function ts(x) { return x.toString() }
 function bs(b) { return (b ? "True" : "False") }
 
-function pf() { alert("Pattern match failure") }
+function pi(s) {
+  var r = parseInt(s);
+  if (r.toString() == s)
+    return r;
+  else
+    throw "Can't parse int: " + s;
+}
+
+function pfl(s) {
+  var r = parseFloat(s);
+  if (r.toString() == s)
+    return r;
+  else
+    throw "Can't parse float: " + s;
+}
+
+function pf() {
+  alert("Pattern match failure");
+  throw "Pattern match failure";
+}
 
 var closures = [];
 
@@ -145,8 +164,10 @@
 
       if (isok)
         k(parse(xhr.responseText));
-      else
+      else {
         alert("Error querying remote server!");
+        throw "Error querying remote server!";
+      }
     }
   };