diff options
Diffstat (limited to 'lib/js/urweb.js')
-rw-r--r-- | lib/js/urweb.js | 18 |
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 + ")"); } |