Batch example

1 files changed, 23 insertions, 2 deletions

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 158e574d..08d96040 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -99,7 +99,26 @@ function eh(x) {
 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 @@ function rc(uri, parse, k) {
 
       if (isok)
         k(parse(xhr.responseText));
-      else
+      else {
         alert("Error querying remote server!");
+        throw "Error querying remote server!";
+      }
     }
   };