aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/js/urweb.js
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-08-09 16:13:27 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-08-09 16:13:27 -0400
commit9f1c85cf0ef4be94bf189dea486806298f09ab51 (patch)
tree007835aa119d7ec7cae1d7de078850147ab9ca13 /lib/js/urweb.js
parentc79947821b62c16f0a5a21fb5ec935c1dba00aae (diff)
Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference
Diffstat (limited to 'lib/js/urweb.js')
-rw-r--r--lib/js/urweb.js18
1 files changed, 15 insertions, 3 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 57ad5454..ef2c7b49 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -306,7 +306,7 @@ function dyn(pnode, s) {
var arr = dummy.getElementsByTagName("tbody");
firstChild = null;
- if (arr.length > 0) {
+ if (arr.length > 0 && table != null) {
var tbody = arr[0], next;
firstChild = document.createElement("script");
table.insertBefore(firstChild, x);
@@ -323,7 +323,7 @@ function dyn(pnode, s) {
var arr = dummy.getElementsByTagName("tr");
firstChild = null;
- if (arr.length > 0) {
+ if (arr.length > 0 && table != null) {
var tbody = arr[0], next;
firstChild = document.createElement("script");
table.insertBefore(firstChild, x);
@@ -468,7 +468,19 @@ function uf(s) {
}
function uu(s) {
- return unescape(s);
+ return unescape(s.replace(new RegExp ("\\+", "g"), " "));
+}
+
+function uul(getToken, getData) {
+ var tok = getToken();
+ if (tok == "Nil") {
+ return null;
+ } else if (tok == "Cons") {
+ var d = getData();
+ var l = uul(getToken, getData);
+ return {_1:d, _2:l};
+ } else
+ throw ("Can't unmarshal list (" + tok + ")");
}