annotate lib/js/urweb.js @ 979:3612ff0c6a10

Main demo pieces all seem to work with interpretation
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Sep 2009 10:50:23 -0400
parents e1f3f1ea8cff
children 6934343267c0
rev   line source
adamc@970 1 // Function versions of operators
adamc@970 2
adamc@970 3 function not(x) { return !x; }
adamc@970 4 function neg(x) { return -x; }
adamc@970 5
adamc@970 6 function eq(x, y) { return x == y; }
adamc@970 7 function plus(x, y) { return x + y; }
adamc@970 8 function minus(x, y) { return x - y; }
adamc@970 9 function times(x, y) { return x * y; }
adamc@970 10 function div(x, y) { return x / y; }
adamc@970 11 function mod(x, y) { return x % y; }
adamc@970 12 function lt(x, y) { return x < y; }
adamc@970 13 function le(x, y) { return x <= y; }
adamc@970 14
adamc@692 15 // Lists
adamc@692 16
adamc@580 17 function cons(v, ls) {
adamc@690 18 return { next : ls, data : v };
adamc@690 19 }
adamc@969 20 function rev(ls) {
adamc@969 21 var acc = null;
adamc@969 22 for (; ls; ls = ls.next)
adamc@969 23 acc = cons(ls.data, acc);
adamc@969 24 return acc;
adamc@969 25 }
adamc@690 26 function concat(ls1, ls2) {
adamc@969 27 var acc = ls2;
adamc@969 28 ls1 = rev(ls1);
adamc@969 29 for (; ls1; ls1 = ls1.next)
adamc@969 30 acc = cons(ls1.data, acc);
adamc@969 31 return acc;
adamc@690 32 }
adamc@690 33 function member(x, ls) {
adamc@690 34 for (; ls; ls = ls.next)
adamc@690 35 if (ls.data == x)
adamc@690 36 return true;
adamc@690 37 return false;
adamc@690 38 }
adamc@690 39 function remove(x, ls) {
adamc@969 40 var acc = null;
adamc@969 41
adamc@969 42 for (; ls; ls = ls.next)
adamc@969 43 if (ls.data == x)
adamc@969 44 return concat(acc, ls.next);
adamc@969 45 else
adamc@969 46 acc = cons(ls.data, acc);
adamc@969 47
adamc@969 48 return ls;
adamc@690 49 }
adamc@690 50 function union(ls1, ls2) {
adamc@969 51 var acc = ls2;
adamc@969 52
adamc@969 53 for (; ls1; ls1 = ls1.next)
adamc@969 54 if (!member(ls1.data, ls2))
adamc@969 55 acc = cons(ls1.data, acc);
adamc@969 56
adamc@969 57 return acc;
adamc@580 58 }
adamc@703 59 function length(ls) {
adamc@969 60 var acc = 0;
adamc@969 61
adamc@969 62 for (; ls; ls = ls.next)
adamc@969 63 ++acc;
adamc@969 64
adamc@969 65 return acc;
adamc@703 66 }
adamc@670 67
adamc@690 68
adamc@729 69 // Error handling
adamc@729 70
adamc@729 71 function whine(msg) {
adamc@729 72 alert(msg);
adamc@729 73 throw msg;
adamc@729 74 }
adamc@729 75
adamc@810 76 function pf(loc) {
adamc@835 77 throw ("Pattern match failure (" + loc + ")");
adamc@729 78 }
adamc@729 79
adamc@798 80 function runHandlers(kind, ls, arg) {
adamc@798 81 if (ls == null)
adamc@798 82 alert(kind + ": " + arg);
adamc@729 83 for (; ls; ls = ls.next)
adamc@729 84 try {
adamc@976 85 exec({c:"a", f:{c:"a", f:ls.data, x:{c:"c", v:arg}}, x:{c:"c", v:null}});
adamc@729 86 } catch (v) { }
adamc@729 87 }
adamc@729 88
adamc@729 89 var errorHandlers = null;
adamc@729 90
adamc@729 91 function onError(f) {
adamc@729 92 errorHandlers = cons(f, errorHandlers);
adamc@729 93 }
adamc@729 94
adamc@729 95 function er(s) {
adamc@798 96 runHandlers("Error", errorHandlers, s);
adamc@729 97 throw {uw_error: s};
adamc@729 98 }
adamc@729 99
adamc@729 100 var failHandlers = null;
adamc@729 101
adamc@729 102 function onFail(f) {
adamc@729 103 failHandlers = cons(f, failHandlers);
adamc@729 104 }
adamc@729 105
adamc@729 106 function doExn(v) {
adamc@729 107 if (v == null || v.uw_error == null) {
adamc@729 108 var s = (v == null ? "null" : v.toString());
adamc@969 109 if (v != null && v.fileName && v.lineNumber)
adamc@969 110 s += " (" + v.fileName + ":" + v.lineNumber + ")";
adamc@798 111 runHandlers("Fail", failHandlers, s);
adamc@729 112 }
adamc@729 113 }
adamc@729 114
adamc@729 115 var disconnectHandlers = null;
adamc@729 116
adamc@976 117 function flift(f) {
adamc@977 118 return {env:cons(f,null), body:{c:"v", n:1}};
adamc@976 119 }
adamc@976 120
adamc@729 121 function onDisconnect(f) {
adamc@976 122 disconnectHandlers = cons(flift(f), disconnectHandlers);
adamc@729 123 }
adamc@729 124
adamc@729 125 function discon() {
adamc@798 126 runHandlers("Disconnect", disconnectHandlers, null);
adamc@729 127 }
adamc@729 128
adamc@729 129 var connectHandlers = null;
adamc@729 130
adamc@729 131 function onConnectFail(f) {
adamc@976 132 connectHandlers = cons(flift(f), connectHandlers);
adamc@729 133 }
adamc@729 134
adamc@729 135 function conn() {
adamc@798 136 runHandlers("Connect", connectHandlers, null);
adamc@729 137 }
adamc@729 138
adamc@729 139 var serverHandlers = null;
adamc@729 140
adamc@729 141 function onServerError(f) {
adamc@729 142 serverHandlers = cons(f, serverHandlers);
adamc@729 143 }
adamc@729 144
adamc@729 145 function servErr(s) {
adamc@824 146 window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0);
adamc@729 147 }
adamc@729 148
adamc@729 149
adamc@692 150 // Embedding closures in XML strings
adamc@692 151
adamc@693 152 function cs(f) {
adamc@693 153 return {closure: f};
adamc@693 154 }
adamc@693 155
adamc@693 156 function isWeird(v) {
adamc@693 157 return v.closure != null || v.cat1 != null;
adamc@693 158 }
adamc@693 159
adamc@692 160 function cat(s1, s2) {
adamc@693 161 if (isWeird(s1) || isWeird(s2))
adamc@693 162 return {cat1: s1, cat2: s2};
adamc@693 163 else
adamc@692 164 return s1 + s2;
adamc@692 165 }
adamc@692 166
adamc@692 167 var closures = [];
adamc@703 168 var freeClosures = null;
adamc@692 169
adamc@692 170 function newClosure(f) {
adamc@703 171 var n;
adamc@703 172 if (freeClosures == null) {
adamc@703 173 n = closures.length;
adamc@703 174 } else {
adamc@703 175 n = freeClosures.data;
adamc@703 176 freeClosures = freeClosures.next;
adamc@703 177 }
adamc@692 178 closures[n] = f;
adamc@692 179 return n;
adamc@692 180 }
adamc@692 181
adamc@703 182 function freeClosure(n) {
adamc@703 183 closures[n] = null;
adamc@703 184 freeClosures = cons(n, freeClosures);
adamc@703 185 }
adamc@703 186
adamc@692 187 function cr(n) {
adamc@975 188 return closures[n];
adamc@692 189 }
adamc@692 190
adamc@703 191 function flatten(cls, tr) {
adamc@693 192 if (tr.cat1 != null)
adamc@703 193 return flatten(cls, tr.cat1) + flatten(cls, tr.cat2);
adamc@703 194 else if (tr.closure != null) {
adamc@703 195 var cl = newClosure(tr.closure);
adamc@703 196 cls.v = cons(cl, cls.v);
adamc@703 197 return "cr(" + cl + ")";
adamc@703 198 } else
adamc@692 199 return tr;
adamc@692 200 }
adamc@692 201
adamc@728 202 function flattenLocal(s) {
adamc@728 203 var cls = {v : null};
adamc@728 204 var r = flatten(cls, s);
adamc@728 205 for (cl = cls.v; cl != null; cl = cl.next)
adamc@728 206 freeClosure(cl.data);
adamc@728 207 return r;
adamc@728 208 }
adamc@728 209
adamc@692 210
adamc@692 211
adamc@692 212 // Dynamic tree management
adamc@692 213
adamc@976 214 var trace = "";
adamc@976 215
adamc@690 216 function populate(node) {
adamc@690 217 var s = node.signal;
adamc@690 218 var oldSources = node.sources;
adamc@729 219 try {
adamc@977 220 var sr = execF(s, null);
adamc@976 221 var newSources = sr._sources;
adamc@690 222
adamc@729 223 for (var sp = oldSources; sp; sp = sp.next)
adamc@729 224 if (!member(sp.data, newSources))
adamc@729 225 sp.data.dyns = remove(node, sp.data.dyns);
adamc@690 226
adamc@729 227 for (var sp = newSources; sp; sp = sp.next)
adamc@729 228 if (!member(sp.data, oldSources))
adamc@729 229 sp.data.dyns = cons(node, sp.data.dyns);
adamc@690 230
adamc@729 231 node.sources = newSources;
adamc@976 232 node.recreate(sr._data);
adamc@729 233 } catch (v) {
adamc@729 234 doExn(v);
adamc@729 235 }
adamc@579 236 }
adamc@574 237
adamc@580 238 function sc(v) {
adamc@690 239 return {data : v, dyns : null};
adamc@580 240 }
adamc@580 241 function sv(s, v) {
adamc@690 242 s.data = v;
adamc@967 243
adamc@690 244 for (var ls = s.dyns; ls; ls = ls.next)
adamc@690 245 if (!ls.dead)
adamc@690 246 populate(ls.data);
adamc@580 247 }
adamc@601 248 function sg(s) {
adamc@690 249 return s.data;
adamc@601 250 }
adamc@579 251
adamc@580 252 function ss(s) {
adamc@976 253 return {env:cons(s, null), body:{c:"r", l:
adamc@976 254 cons({n:"sources", v:{c:"c", v:cons(s, null)}},
adamc@976 255 cons({n:"data", v:{c:"f", f:sg, a:cons({c:"v", n:1}, null)}}, null))}};
adamc@580 256 }
adamc@580 257 function sr(v) {
adamc@976 258 return {env:null, body:{c:"c", v:{_sources : null, _data : v}}};
adamc@580 259 }
adamc@580 260 function sb(x,y) {
adamc@976 261 return {env:cons(y,cons(x,null)),
adamc@976 262 body:{c:"=",
adamc@977 263 e1:{c:"a", f:{c:"v", n:2}, x:{c:"c", v:null}},
adamc@976 264 e2:{c:"=",
adamc@976 265 e1:{c:"a",
adamc@977 266 f:{c:"a", f:{c:"v", n:2}, x:{c:".", r:{c:"v", n:0}, f:"data"}},
adamc@976 267 x:{c:"c", v:null}},
adamc@976 268 e2:{c:"r", l:cons(
adamc@976 269 {n:"sources", v:{c:"f", f:union, a:cons({c:".", r:{c:"v", n:1}, f:"sources"},
adamc@976 270 cons({c:".", r:{c:"v", n:0}, f:"sources"}, null))}},
adamc@976 271 cons({n:"data", v:{c:".", r:{c:"v", n:0}, f:"data"}}, null))}}}};
adamc@580 272 }
adamc@841 273 function scur(s) {
adamc@976 274 return exec(s).data;
adamc@841 275 }
adamc@571 276
adamc@604 277 function lastParent() {
adamc@604 278 var pos = document;
adamc@604 279
adamc@600 280 while (pos.lastChild && pos.lastChild.nodeType == 1)
adamc@600 281 pos = pos.lastChild;
adamc@600 282
adamc@600 283 return pos.parentNode;
adamc@600 284 }
adamc@600 285
adamc@898 286 function parent() {
adamc@898 287 return thisScript ? thisScript.parentNode : lastParent();
adamc@898 288 }
adamc@898 289
adamc@604 290 function addNode(node) {
adamc@899 291 if (thisScript)
adamc@899 292 thisScript.parentNode.replaceChild(node, thisScript);
adamc@899 293 else
adamc@604 294 lastParent().appendChild(node);
adamc@603 295 }
adamc@603 296
adamc@690 297 var thisScript = null;
adamc@690 298
adamc@604 299 function runScripts(node) {
adamc@899 300 if (node.getElementsByTagName) {
adamc@899 301 var savedScript = thisScript;
adamc@603 302
adamc@899 303 var scripts = node.getElementsByTagName("script"), scriptsCopy = [];
adamc@899 304 var len = scripts.length;
adamc@899 305 for (var i = 0; i < len; ++i)
adamc@899 306 scriptsCopy[i] = scripts[i];
adamc@899 307 for (var i = 0; i < len; ++i) {
adamc@899 308 thisScript = scriptsCopy[i];
adamc@899 309 try {
adamc@899 310 eval(thisScript.textContent);
adamc@899 311 } catch (v) {
adamc@899 312 doExn(v);
adamc@899 313 }
adamc@899 314 if (thisScript.parentNode)
adamc@901 315 thisScript.parentNode.removeChild(thisScript);
adamc@729 316 }
adamc@899 317
adamc@899 318 thisScript = savedScript;
adamc@604 319 }
adamc@603 320 }
adamc@603 321
adamc@603 322
adamc@692 323 // Dynamic tree entry points
adamc@692 324
adamc@967 325 function killScript(scr) {
adamc@967 326 scr.dead = true;
adamc@967 327 for (var ls = scr.sources; ls; ls = ls.next)
adamc@967 328 ls.data.dyns = remove(scr, ls.data.dyns);
adamc@967 329 for (var ls = scr.closures; ls; ls = ls.next)
adamc@967 330 freeClosure(ls.data);
adamc@967 331 }
adamc@967 332
adamc@901 333 function dyn(pnode, s) {
adamc@901 334 var x = document.createElement("script");
adamc@690 335 x.dead = false;
adamc@690 336 x.signal = s;
adamc@690 337 x.sources = null;
adamc@703 338 x.closures = null;
adamc@899 339
adamc@902 340 var firstChild = null;
adamc@899 341
adamc@690 342 x.recreate = function(v) {
adamc@703 343 for (var ls = x.closures; ls; ls = ls.next)
adamc@703 344 freeClosure(ls.data);
adamc@692 345
adamc@902 346 var next;
adamc@902 347 for (var child = firstChild; child && child != x; child = next) {
adamc@902 348 next = child.nextSibling;
adamc@967 349 killScript(child);
adamc@901 350 if (child.getElementsByTagName) {
adamc@901 351 var arr = child.getElementsByTagName("script");
adamc@967 352 for (var i = 0; i < arr.length; ++i)
adamc@967 353 killScript(arr[i]);
adamc@847 354 }
adamc@847 355
adamc@901 356 if (child.parentNode)
adamc@901 357 child.parentNode.removeChild(child);
adamc@899 358 }
adamc@690 359
adamc@703 360 var cls = {v : null};
adamc@901 361 var html = flatten(cls, v);
adamc@703 362 x.closures = cls.v;
adamc@899 363
adamc@901 364 if (pnode == "table") {
adamc@901 365 var dummy = document.createElement("body");
adamc@901 366 dummy.innerHTML = "<table>" + html + "</table>";
adamc@901 367 runScripts(dummy);
adamc@901 368 var table = x.parentNode;
adamc@901 369
adamc@946 370 if (table) {
adamc@946 371 var arr = dummy.getElementsByTagName("tbody");
adamc@946 372 firstChild = null;
adamc@946 373 var tbody;
adamc@946 374 if (arr.length > 0 && table != null)
adamc@946 375 tbody = arr[0];
adamc@946 376 else
adamc@946 377 tbody = dummy.firstChild;
adamc@945 378
adamc@946 379 var next;
adamc@946 380 firstChild = document.createElement("script");
adamc@946 381 table.insertBefore(firstChild, x);
adamc@946 382 for (var node = tbody.firstChild; node; node = next) {
adamc@946 383 next = node.nextSibling;
adamc@946 384 table.insertBefore(node, x);
adamc@946 385 }
adamc@901 386 }
adamc@903 387 } else if (pnode == "tr") {
adamc@903 388 var dummy = document.createElement("body");
adamc@903 389 dummy.innerHTML = "<table><tr>" + html + "</tr></table>";
adamc@903 390 runScripts(dummy);
adamc@903 391 var table = x.parentNode;
adamc@903 392
adamc@946 393 if (table) {
adamc@946 394 var arr = dummy.getElementsByTagName("tr");
adamc@946 395 firstChild = null;
adamc@946 396 var tbody;
adamc@946 397 if (arr.length > 0 && table != null)
adamc@946 398 tbody = arr[0];
adamc@946 399 else
adamc@946 400 tbody = dummy.firstChild;
adamc@946 401
adamc@946 402 var next;
adamc@903 403 firstChild = document.createElement("script");
adamc@903 404 table.insertBefore(firstChild, x);
adamc@903 405 for (var node = tbody.firstChild; node; node = next) {
adamc@903 406 next = node.nextSibling;
adamc@903 407 table.insertBefore(node, x);
adamc@903 408 }
adamc@903 409 }
adamc@901 410 } else {
adamc@902 411 firstChild = document.createElement("span");
adamc@902 412 firstChild.innerHTML = html;
adamc@902 413 runScripts(firstChild);
adamc@900 414 if (x.parentNode)
adamc@902 415 x.parentNode.insertBefore(firstChild, x);
adamc@899 416 }
adamc@690 417 };
adamc@899 418
adamc@899 419 addNode(x);
adamc@690 420 populate(x);
adamc@571 421 }
adamc@582 422
adamc@817 423 function input(t, s, recreate) {
adamc@598 424 var x = document.createElement(t);
adamc@690 425 x.dead = false;
adamc@690 426 x.signal = ss(s);
adamc@690 427 x.sources = null;
adamc@817 428 x.recreate = recreate(x);
adamc@899 429 addNode(x);
adamc@690 430 populate(x);
adamc@816 431
adamc@816 432 return x;
adamc@816 433 }
adamc@816 434
adamc@816 435 function inp(s) {
adamc@817 436 var x = input("input", s, function(x) { return function(v) { if (x.value != v) x.value = v; }; });
adamc@816 437 x.value = s.data;
adamc@816 438 x.onkeyup = function() { sv(s, x.value) };
adamc@816 439
adamc@816 440 return x;
adamc@816 441 }
adamc@816 442
adamc@816 443 function sel(s, content) {
adamc@817 444 var x = input("select", s, function(x) { return function(v) { if (x.value != v) x.value = v; }; });
adamc@816 445 x.innerHTML = content;
adamc@816 446 x.value = s.data;
adamc@835 447 if (x.value != s.data)
adamc@835 448 sv(s, x.value);
adamc@816 449 x.onchange = function() { sv(s, x.value) };
adamc@797 450
adamc@606 451 return x;
adamc@598 452 }
adamc@598 453
adamc@817 454 function chk(s) {
adamc@817 455 var x = input("input", s, function(x) { return function(v) { if (x.checked != v) x.checked = v; }; });
adamc@817 456 x.type = "checkbox";
adamc@817 457 x.checked = s.data;
adamc@817 458 x.onchange = function() { sv(s, x.checked) };
adamc@817 459
adamc@817 460 return x;
adamc@817 461 }
adamc@817 462
adamc@800 463 function addOnChange(x, f) {
adamc@800 464 var old = x.onchange;
adamc@800 465 x.onchange = function() { old(); f (); };
adamc@800 466 }
adamc@800 467
adamc@692 468
adamc@692 469 // Basic string operations
adamc@692 470
adamc@597 471 function eh(x) {
adamc@800 472 if (x == null)
adamc@800 473 return "NULL";
adamc@800 474 else
adamc@800 475 return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
adamc@597 476 }
adamc@597 477
adamc@582 478 function ts(x) { return x.toString() }
adamc@586 479 function bs(b) { return (b ? "True" : "False") }
adamc@586 480
adamc@828 481 function sub(s, i) { return s[i]; }
adamc@828 482 function suf(s, i) { return s.substring(i); }
adamc@828 483 function slen(s) { return s.length; }
adamc@829 484 function sidx(s, ch) {
adamc@829 485 var r = s.indexOf(ch);
adamc@829 486 if (r == -1)
adamc@829 487 return null;
adamc@829 488 else
adamc@829 489 return r;
adamc@829 490 }
adamc@831 491 function sspn(s, chs) {
adamc@831 492 for (var i = 0; i < s.length; ++i)
adamc@831 493 if (chs.indexOf(s[i]) != -1)
adamc@831 494 return i;
adamc@831 495
adamc@831 496 return null;
adamc@831 497 }
adamc@829 498 function schr(s, ch) {
adamc@829 499 var r = s.indexOf(ch);
adamc@829 500 if (r == -1)
adamc@829 501 return null;
adamc@829 502 else
adamc@829 503 return s.substring(r);
adamc@829 504 }
adamc@829 505 function ssub(s, start, len) {
adamc@829 506 return s.substring(start, start+len);
adamc@829 507 }
adamc@821 508
adamc@649 509 function pi(s) {
adamc@649 510 var r = parseInt(s);
adamc@649 511 if (r.toString() == s)
adamc@649 512 return r;
adamc@649 513 else
adamc@729 514 er("Can't parse int: " + s);
adamc@649 515 }
adamc@649 516
adamc@649 517 function pfl(s) {
adamc@649 518 var r = parseFloat(s);
adamc@649 519 if (r.toString() == s)
adamc@649 520 return r;
adamc@649 521 else
adamc@729 522 er("Can't parse float: " + s);
adamc@649 523 }
adamc@649 524
adamc@838 525 function pio(s) {
adamc@838 526 var r = parseInt(s);
adamc@838 527 if (r.toString() == s)
adamc@838 528 return r;
adamc@838 529 else
adamc@838 530 return null;
adamc@838 531 }
adamc@838 532
adamc@838 533 function pflo(s) {
adamc@838 534 var r = parseFloat(s);
adamc@838 535 if (r.toString() == s)
adamc@838 536 return r;
adamc@838 537 else
adamc@838 538 return null;
adamc@838 539 }
adamc@838 540
adamc@692 541 function uf(s) {
adamc@925 542 if (s.length == 0)
adamc@925 543 return "_";
adamc@925 544 return (s[0] == '_' ? "_" : "")
adamc@925 545 + escape(s).replace(new RegExp ("/", "g"), "%2F").replace(new RegExp ("\\+", "g"), "%2B");
adamc@691 546 }
adamc@691 547
adamc@692 548 function uu(s) {
adamc@925 549 if (s.length > 0 && s[0] == '_')
adamc@925 550 s = s.substring(1);
adamc@927 551 else if (s.length >= 3 && s[0] == '%' && s[1] == '5' && (s[2] == 'f' || s[2] == 'F'))
adamc@927 552 s = s.substring(3);
adamc@905 553 return unescape(s.replace(new RegExp ("\\+", "g"), " "));
adamc@905 554 }
adamc@905 555
adamc@912 556 function ub(b) {
adamc@912 557 return b ? "1" : "0";
adamc@912 558 }
adamc@912 559
adamc@905 560 function uul(getToken, getData) {
adamc@905 561 var tok = getToken();
adamc@905 562 if (tok == "Nil") {
adamc@905 563 return null;
adamc@905 564 } else if (tok == "Cons") {
adamc@905 565 var d = getData();
adamc@905 566 var l = uul(getToken, getData);
adamc@905 567 return {_1:d, _2:l};
adamc@905 568 } else
adamc@905 569 throw ("Can't unmarshal list (" + tok + ")");
adamc@692 570 }
adamc@692 571
adamc@961 572 function strcmp(str1, str2) {
adamc@961 573 return ((str1 == str2) ? 0 : ((str1 > str2) ? 1 : -1));
adamc@961 574 }
adamc@692 575
adamc@603 576
adamc@692 577 // Remote calls
adamc@609 578
adamc@703 579 var client_id = null;
adamc@668 580 var client_pass = 0;
adamc@668 581 var url_prefix = "/";
adamc@673 582 var timeout = 60;
adamc@668 583
adamc@668 584 function getXHR(uri)
adamc@609 585 {
adamc@609 586 try {
adamc@609 587 return new XMLHttpRequest();
adamc@609 588 } catch (e) {
adamc@609 589 try {
adamc@609 590 return new ActiveXObject("Msxml2.XMLHTTP");
adamc@609 591 } catch (e) {
adamc@609 592 try {
adamc@609 593 return new ActiveXObject("Microsoft.XMLHTTP");
adamc@609 594 } catch (e) {
adamc@609 595 throw "Your browser doesn't seem to support AJAX.";
adamc@609 596 }
adamc@609 597 }
adamc@609 598 }
adamc@609 599 }
adamc@609 600
adamc@736 601 var sig = null;
adamc@736 602
adamc@736 603 function requestUri(xhr, uri, needsSig) {
adamc@668 604 xhr.open("GET", uri, true);
adamc@668 605
adamc@703 606 if (client_id != null) {
adamc@668 607 xhr.setRequestHeader("UrWeb-Client", client_id.toString());
adamc@668 608 xhr.setRequestHeader("UrWeb-Pass", client_pass.toString());
adamc@668 609 }
adamc@668 610
adamc@736 611 if (needsSig) {
adamc@736 612 if (sig == null)
adamc@736 613 whine("Missing cookie signature!");
adamc@736 614
adamc@736 615 xhr.setRequestHeader("UrWeb-Sig", sig);
adamc@736 616 }
adamc@736 617
adamc@668 618 xhr.send(null);
adamc@668 619 }
adamc@668 620
adamc@978 621 function rc(prefix, uri, parse, k, needsSig) {
adamc@978 622 uri = cat(prefix, uri);
adamc@728 623 uri = flattenLocal(uri);
adamc@609 624 var xhr = getXHR();
adamc@609 625
adamc@609 626 xhr.onreadystatechange = function() {
adamc@612 627 if (xhr.readyState == 4) {
adamc@612 628 var isok = false;
adamc@612 629
adamc@612 630 try {
adamc@612 631 if (xhr.status == 200)
adamc@612 632 isok = true;
adamc@612 633 } catch (e) { }
adamc@612 634
adamc@729 635 if (isok) {
adamc@729 636 try {
adamc@977 637 execF(k, parse(xhr.responseText));
adamc@729 638 } catch (v) {
adamc@729 639 doExn(v);
adamc@729 640 }
adamc@729 641 } else {
adamc@729 642 conn();
adamc@649 643 }
adamc@612 644 }
adamc@609 645 };
adamc@609 646
adamc@736 647 requestUri(xhr, uri, needsSig);
adamc@609 648 }
adamc@667 649
adamc@667 650 function path_join(s1, s2) {
adamc@667 651 if (s1.length > 0 && s1[s1.length-1] == '/')
adamc@667 652 return s1 + s2;
adamc@667 653 else
adamc@667 654 return s1 + "/" + s2;
adamc@667 655 }
adamc@667 656
adamc@670 657 var channels = [];
adamc@670 658
adamc@670 659 function newQueue() {
adamc@670 660 return { front : null, back : null };
adamc@670 661 }
adamc@670 662 function enqueue(q, v) {
adamc@670 663 if (q.front == null) {
adamc@670 664 q.front = cons(v, null);
adamc@670 665 q.back = q.front;
adamc@670 666 } else {
adamc@670 667 var node = cons(v, null);
adamc@690 668 q.back.next = node;
adamc@670 669 q.back = node;
adamc@670 670 }
adamc@670 671 }
adamc@670 672 function dequeue(q) {
adamc@670 673 if (q.front == null)
adamc@670 674 return null;
adamc@670 675 else {
adamc@690 676 var r = q.front.data;
adamc@690 677 q.front = q.front.next;
adamc@670 678 if (q.front == null)
adamc@670 679 q.back = null;
adamc@670 680 return r;
adamc@670 681 }
adamc@670 682 }
adamc@670 683
adamc@670 684 function newChannel() {
adamc@670 685 return { msgs : newQueue(), listeners : newQueue() };
adamc@670 686 }
adamc@670 687
adamc@667 688 function listener() {
adamc@668 689 var uri = path_join(url_prefix, ".msgs");
adamc@667 690 var xhr = getXHR();
adamc@673 691 var tid, orsc, onTimeout;
adamc@673 692
adamc@673 693 var connect = function () {
adamc@673 694 xhr.onreadystatechange = orsc;
adamc@673 695 tid = window.setTimeout(onTimeout, timeout * 500);
adamc@736 696 requestUri(xhr, uri, false);
adamc@673 697 }
adamc@673 698
adamc@673 699 orsc = function() {
adamc@667 700 if (xhr.readyState == 4) {
adamc@673 701 window.clearTimeout(tid);
adamc@673 702
adamc@667 703 var isok = false;
adamc@667 704
adamc@667 705 try {
adamc@667 706 if (xhr.status == 200)
adamc@667 707 isok = true;
adamc@667 708 } catch (e) { }
adamc@667 709
adamc@668 710 if (isok) {
adamc@889 711 var text = xhr.responseText
adamc@889 712 if (text == "")
adamc@889 713 return;
adamc@889 714 var lines = text.split("\n");
adamc@889 715
adamc@729 716 if (lines.length < 2) {
adamc@729 717 discon();
adamc@729 718 return;
adamc@729 719 }
adamc@669 720
adamc@669 721 for (var i = 0; i+1 < lines.length; i += 2) {
adamc@670 722 var chn = lines[i];
adamc@670 723 var msg = lines[i+1];
adamc@670 724
adamc@670 725 if (chn < 0)
adamc@670 726 whine("Out-of-bounds channel in message from remote server");
adamc@670 727
adamc@670 728 var ch;
adamc@670 729
adamc@670 730 if (chn >= channels.length || channels[chn] == null) {
adamc@670 731 ch = newChannel();
adamc@670 732 channels[chn] = ch;
adamc@670 733 } else
adamc@670 734 ch = channels[chn];
adamc@670 735
adamc@670 736 var listener = dequeue(ch.listeners);
adamc@670 737 if (listener == null) {
adamc@670 738 enqueue(ch.msgs, msg);
adamc@670 739 } else {
adamc@728 740 try {
adamc@728 741 listener(msg);
adamc@728 742 } catch (v) {
adamc@728 743 doExn(v);
adamc@728 744 }
adamc@670 745 }
adamc@669 746 }
adamc@669 747
adamc@673 748 connect();
adamc@668 749 }
adamc@667 750 else {
adamc@729 751 try {
adamc@824 752 if (xhr.status != 0)
adamc@824 753 servErr("Error querying remote server for messages: " + xhr.status);
adamc@889 754 } catch (e) { }
adamc@667 755 }
adamc@667 756 }
adamc@667 757 };
adamc@667 758
adamc@673 759 onTimeout = function() {
adamc@673 760 xhr.abort();
adamc@673 761 connect();
adamc@673 762 };
adamc@673 763
adamc@673 764 connect();
adamc@667 765 }
adamc@670 766
adamc@670 767 function rv(chn, parse, k) {
adamc@682 768 if (chn == null)
adamc@682 769 return;
adamc@682 770
adamc@670 771 if (chn < 0)
adamc@670 772 whine("Out-of-bounds channel receive");
adamc@670 773
adamc@670 774 var ch;
adamc@670 775
adamc@670 776 if (chn >= channels.length || channels[chn] == null) {
adamc@670 777 ch = newChannel();
adamc@670 778 channels[chn] = ch;
adamc@670 779 } else
adamc@670 780 ch = channels[chn];
adamc@670 781
adamc@670 782 var msg = dequeue(ch.msgs);
adamc@670 783 if (msg == null) {
adamc@979 784 enqueue(ch.listeners, function(msg) { execF(execF(k, parse(msg)), null); });
adamc@670 785 } else {
adamc@728 786 try {
adamc@977 787 execF(execF(k, parse(msg)), null);
adamc@728 788 } catch (v) {
adamc@728 789 doExn(v);
adamc@728 790 }
adamc@670 791 }
adamc@670 792 }
adamc@693 793
adamc@978 794 function sl(ms, k) {
adamc@978 795 window.setTimeout(function() { execF(k, null); }, ms);
adamc@978 796 }
adamc@978 797
adamc@693 798
adamc@895 799 // Key events
adamc@895 800
adamc@970 801 var uw_event = null;
adamc@970 802
adamc@970 803 function kc() {
adamc@970 804 return window.event ? uw_event.keyCode : uw_event.which;
adamc@970 805 }
adamc@970 806
adamc@970 807
adamc@970 808 // The Ur interpreter
adamc@970 809
adamc@970 810 var urfuncs = [];
adamc@970 811
adamc@970 812 function lookup(env, n) {
adamc@970 813 while (env != null) {
adamc@970 814 if (n == 0)
adamc@970 815 return env.data;
adamc@970 816 else {
adamc@970 817 --n;
adamc@970 818 env = env.next;
adamc@970 819 }
adamc@970 820 }
adamc@970 821
adamc@970 822 throw "Out-of-bounds Ur variable reference";
adamc@970 823 }
adamc@970 824
adamc@974 825 function execP(env, p, v) {
adamc@974 826 switch (p.c) {
adamc@974 827 case "w":
adamc@974 828 return env;
adamc@974 829 case "v":
adamc@974 830 return cons(v, env);
adamc@974 831 case "c":
adamc@974 832 if (v == p.v)
adamc@974 833 return env;
adamc@974 834 else
adamc@974 835 return false;
adamc@974 836 case "s":
adamc@974 837 if (v == null)
adamc@974 838 return false;
adamc@974 839 else
adamc@974 840 return execP(env, p.p, p.n ? v.v : v);
adamc@974 841 case "1":
adamc@974 842 if (v.n != p.n)
adamc@974 843 return false;
adamc@974 844 else
adamc@974 845 return execP(env, p.p, v.v);
adamc@974 846 case "r":
adamc@974 847 for (var fs = p.l; fs != null; fs = fs.next) {
adamc@974 848 env = execP(env, fs.data.p, v["_" + fs.data.n]);
adamc@974 849 if (env == false)
adamc@974 850 return false;
adamc@974 851 }
adamc@974 852 return env;
adamc@974 853 default:
adamc@974 854 throw ("Unknown Ur pattern kind" + p.c);
adamc@974 855 }
adamc@974 856 }
adamc@974 857
adamc@970 858 function exec0(env, e) {
adamc@970 859 var stack = null;
adamc@970 860
adamc@970 861 while (true) {
adamc@970 862 switch (e.c) {
adamc@970 863 case "c":
adamc@970 864 var v = e.v;
adamc@970 865 if (stack == null)
adamc@970 866 return v;
adamc@970 867 var fr = stack.data;
adamc@970 868
adamc@970 869 switch (fr.c) {
adamc@970 870 case "s":
adamc@970 871 e = {c: "c", v: {v: v}};
adamc@970 872 stack = stack.next;
adamc@970 873 break;
adamc@970 874 case "1":
adamc@970 875 e = {c: "c", v: {n: fr.n, v: v}};
adamc@970 876 stack = stack.next;
adamc@970 877 break;
adamc@970 878 case "f":
adamc@970 879 fr.args[fr.pos++] = v;
adamc@970 880 if (fr.a == null) {
adamc@970 881 e = {c: "c", v: fr.f.apply(null, fr.args)};
adamc@970 882 stack = stack.next;
adamc@970 883 } else {
adamc@978 884 trace += "" + fr.pos;
adamc@970 885 e = fr.a.data;
adamc@970 886 fr.a = fr.a.next;
adamc@970 887 }
adamc@970 888 break;
adamc@970 889 case "a1":
adamc@970 890 e = fr.x;
adamc@971 891 stack = cons({c: "a2", f: v}, stack.next);
adamc@970 892 break;
adamc@970 893 case "a2":
adamc@971 894 if (fr.f == null)
adamc@971 895 throw "Ur: applying null function";
adamc@971 896 else if (fr.f.body) {
adamc@978 897 stack = cons({c: "<", env: env}, stack.next);
adamc@971 898 env = cons(v, fr.f.env);
adamc@971 899 e = fr.f.body;
adamc@971 900 } else {
adamc@971 901 e = {c: "c", v: fr.f(v)};
adamc@971 902 stack = stack.next;
adamc@971 903 }
adamc@970 904 break;
adamc@978 905 case "<":
adamc@970 906 env = fr.env;
adamc@970 907 stack = stack.next;
adamc@970 908 break;
adamc@970 909 case "r":
adamc@970 910 fr.fs["_" + fr.n] = v;
adamc@970 911 if (fr.l == null) {
adamc@970 912 e = {c: "c", v: fr.fs};
adamc@970 913 stack = stack.next;
adamc@970 914 } else {
adamc@970 915 fr.n = fr.l.data.n;
adamc@970 916 e = fr.l.data.v;
adamc@970 917 fr.l = fr.l.next;
adamc@970 918 }
adamc@970 919 break;
adamc@970 920 case ".":
adamc@970 921 e = {c: "c", v: v["_" + fr.f]};
adamc@970 922 stack = stack.next;
adamc@970 923 break;
adamc@970 924 case ";":
adamc@970 925 e = fr.e2;
adamc@970 926 stack = stack.next;
adamc@970 927 break;
adamc@970 928 case "=":
adamc@978 929 stack = cons({c: "<", env: env}, stack.next);
adamc@970 930 env = cons(v, env);
adamc@970 931 e = fr.e2;
adamc@970 932 break;
adamc@974 933 case "m":
adamc@974 934 var ps;
adamc@974 935 for (ps = fr.p; ps != null; ps = ps.next) {
adamc@974 936 var r = execP(env, ps.data.p, v);
adamc@974 937 if (r != false) {
adamc@978 938 stack = cons({c: "<", env: env}, stack.next);
adamc@974 939 env = r;
adamc@974 940 e = ps.data.b;
adamc@974 941 break;
adamc@974 942 }
adamc@974 943 }
adamc@974 944 if (ps == null)
adamc@974 945 throw "Match failure in Ur interpretation";
adamc@974 946 break;
adamc@970 947 default:
adamc@973 948 throw ("Unknown Ur continuation kind " + fr.c);
adamc@970 949 }
adamc@970 950
adamc@970 951 break;
adamc@970 952 case "v":
adamc@970 953 e = {c: "c", v: lookup(env, e.n)};
adamc@970 954 break;
adamc@970 955 case "n":
adamc@971 956 e = urfuncs[e.n];
adamc@970 957 break;
adamc@970 958 case "s":
adamc@970 959 stack = cons({c: "s"}, stack);
adamc@970 960 e = e.v;
adamc@970 961 break;
adamc@970 962 case "1":
adamc@970 963 stack = cons({c: "1", n: e.n}, stack);
adamc@970 964 e = e.v;
adamc@970 965 break;
adamc@970 966 case "f":
adamc@970 967 if (e.a == null)
adamc@970 968 e = {c: "c", v: e.f()};
adamc@970 969 else {
adamc@970 970 var args = [];
adamc@970 971 stack = cons({c: "f", f: e.f, args: args, pos: 0, a: e.a.next}, stack);
adamc@970 972 e = e.a.data;
adamc@970 973 }
adamc@970 974 break;
adamc@970 975 case "l":
adamc@970 976 e = {c: "c", v: {env: env, body: e.b}};
adamc@970 977 break;
adamc@970 978 case "a":
adamc@970 979 stack = cons({c: "a1", x: e.x}, stack);
adamc@970 980 e = e.f;
adamc@970 981 break;
adamc@970 982 case "r":
adamc@970 983 if (e.l == null)
adamc@970 984 throw "Empty Ur record in interpretation";
adamc@970 985 var fs = {};
adamc@970 986 stack = cons({c: "r", n: e.l.data.n, fs: fs, l: e.l.next}, stack);
adamc@973 987 e = e.l.data.v;
adamc@970 988 break;
adamc@970 989 case ".":
adamc@970 990 stack = cons({c: ".", f: e.f}, stack);
adamc@970 991 e = e.r;
adamc@970 992 break;
adamc@970 993 case ";":
adamc@970 994 stack = cons({c: ";", e2: e.e2}, stack);
adamc@970 995 e = e.e1;
adamc@970 996 break;
adamc@970 997 case "=":
adamc@970 998 stack = cons({c: "=", e2: e.e2}, stack);
adamc@970 999 e = e.e1;
adamc@970 1000 break;
adamc@974 1001 case "m":
adamc@974 1002 stack = cons({c: "m", p: e.p}, stack);
adamc@974 1003 e = e.e;
adamc@974 1004 break;
adamc@970 1005 case "e":
adamc@975 1006 e = {c: "c", v: cs({c: "wc", env: env, body: e.e})};
adamc@975 1007 break;
adamc@975 1008 case "wc":
adamc@975 1009 env = e.env;
adamc@975 1010 e = e.body;
adamc@970 1011 break;
adamc@970 1012 default:
adamc@973 1013 throw ("Unknown Ur expression kind " + e.c);
adamc@970 1014 }
adamc@970 1015 }
adamc@970 1016 }
adamc@970 1017
adamc@976 1018 function execD(e) {
adamc@976 1019 return exec0(null, e);
adamc@976 1020 }
adamc@976 1021
adamc@970 1022 function exec(e) {
adamc@970 1023 var r = exec0(null, e);
adamc@970 1024
adamc@975 1025 if (r != null && r.body != null)
adamc@970 1026 return function(v) { return exec0(cons(v, r.env), r.body); };
adamc@970 1027 else
adamc@970 1028 return r;
adamc@895 1029 }
adamc@895 1030
adamc@977 1031 function execF(f, x) {
adamc@977 1032 return exec0(cons(x, f.env), f.body);
adamc@977 1033 }
adamc@977 1034
adamc@895 1035
adamc@693 1036 // App-specific code
adamc@693 1037