summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 15:17:23 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 15:17:23 -0400
commitb8e7b835e7cde4cf374138467da8b16e93a65eb9 (patch)
tree433f576bae7ae3c50abfef5327d67f0220601783 /lib
parent4f9024019d78bebec6926d19da0361587c88bd03 (diff)
Batch example
Diffstat (limited to 'lib')
-rw-r--r--lib/js/urweb.js25
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!";
+ }
}
};