annotate lib/js/urweb.js @ 641:b98f547a6a45

RPC returning an option
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Mar 2009 13:41:55 -0400
parents c5991cdb0c4b
children fb2a0e76dcef
rev   line source
adamc@580 1 function cons(v, ls) {
adamc@580 2 return { n : ls, v : v };
adamc@580 3 }
adamc@579 4 function callAll(ls) {
adamc@585 5 for (; ls; ls = ls.n)
adamc@579 6 ls.v();
adamc@579 7 }
adamc@574 8
adamc@580 9 function sc(v) {
adamc@580 10 return {v : v, h : null};
adamc@580 11 }
adamc@580 12 function sv(s, v) {
adamc@580 13 s.v = v;
adamc@580 14 callAll(s.h);
adamc@580 15 }
adamc@601 16 function sg(s) {
adamc@601 17 return s.v;
adamc@601 18 }
adamc@579 19
adamc@580 20 function ss(s) {
adamc@580 21 return s;
adamc@580 22 }
adamc@580 23 function sr(v) {
adamc@580 24 return {v : v, h : null};
adamc@580 25 }
adamc@580 26 function sb(x,y) {
adamc@580 27 var z = y(x.v);
adamc@580 28 var s = {v : z.v, h : null};
adamc@580 29
adamc@580 30 function reZ() {
adamc@580 31 z.h = cons(function() { s.v = z.v; callAll(s.h); }, z.h);
adamc@580 32 }
adamc@580 33
adamc@580 34 x.h = cons(function() { z = y(x.v); reZ(); s.v = z.v; callAll(s.h); }, x.h);
adamc@580 35 reZ();
adamc@580 36
adamc@580 37 return s;
adamc@580 38 }
adamc@571 39
adamc@604 40 function lastParent() {
adamc@604 41 var pos = document;
adamc@604 42
adamc@600 43 while (pos.lastChild && pos.lastChild.nodeType == 1)
adamc@600 44 pos = pos.lastChild;
adamc@600 45
adamc@600 46 return pos.parentNode;
adamc@600 47 }
adamc@600 48
adamc@604 49 var thisScript = null;
adamc@603 50
adamc@604 51 function addNode(node) {
adamc@604 52 if (thisScript) {
adamc@604 53 thisScript.parentNode.appendChild(node);
adamc@604 54 thisScript.parentNode.removeChild(thisScript);
adamc@604 55 } else
adamc@604 56 lastParent().appendChild(node);
adamc@603 57 }
adamc@603 58
adamc@604 59 function runScripts(node) {
adamc@604 60 var savedScript = thisScript;
adamc@603 61
adamc@604 62 var scripts = node.getElementsByTagName("script");
adamc@604 63 var len = scripts.length;
adamc@604 64 for (var i = 0; i < len; ++i) {
adamc@604 65 thisScript = scripts[i];
adamc@604 66 eval(thisScript.textContent);
adamc@604 67 }
adamc@604 68
adamc@604 69 thisScript = savedScript;
adamc@603 70 }
adamc@603 71
adamc@603 72 function populate(node, html) {
adamc@603 73 node.innerHTML = html;
adamc@604 74 runScripts(node);
adamc@603 75 }
adamc@603 76
adamc@571 77 function dyn(s) {
adamc@571 78 var x = document.createElement("span");
adamc@604 79 populate(x, s.v);
adamc@604 80 addNode(x);
adamc@603 81 s.h = cons(function() { populate(x, s.v) }, s.h);
adamc@571 82 }
adamc@582 83
adamc@598 84 function inp(t, s) {
adamc@598 85 var x = document.createElement(t);
adamc@598 86 x.value = s.v;
adamc@604 87 addNode(x);
adamc@598 88 s.h = cons(function() { x.value = s.v }, s.h);
adamc@598 89 x.onkeyup = function() { sv(s, x.value) };
adamc@606 90 return x;
adamc@598 91 }
adamc@598 92
adamc@597 93 function eh(x) {
adamc@597 94 return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
adamc@597 95 }
adamc@597 96
adamc@582 97 function ts(x) { return x.toString() }
adamc@586 98 function bs(b) { return (b ? "True" : "False") }
adamc@586 99
adamc@584 100 function pf() { alert("Pattern match failure") }
adamc@589 101
adamc@603 102 var closures = [];
adamc@603 103
adamc@603 104 function ca(f) {
adamc@603 105 var n = closures.length;
adamc@603 106 closures[n] = f;
adamc@603 107 return n;
adamc@603 108 }
adamc@603 109
adamc@603 110 function cr(n) {
adamc@603 111 return closures[n]();
adamc@603 112 }
adamc@603 113
adamc@609 114
adamc@609 115 function getXHR()
adamc@609 116 {
adamc@609 117 try {
adamc@609 118 return new XMLHttpRequest();
adamc@609 119 } catch (e) {
adamc@609 120 try {
adamc@609 121 return new ActiveXObject("Msxml2.XMLHTTP");
adamc@609 122 } catch (e) {
adamc@609 123 try {
adamc@609 124 return new ActiveXObject("Microsoft.XMLHTTP");
adamc@609 125 } catch (e) {
adamc@609 126 throw "Your browser doesn't seem to support AJAX.";
adamc@609 127 }
adamc@609 128 }
adamc@609 129 }
adamc@609 130 }
adamc@609 131
adamc@613 132 function rc(uri, parse, k) {
adamc@609 133 var xhr = getXHR();
adamc@609 134
adamc@609 135 xhr.onreadystatechange = function() {
adamc@612 136 if (xhr.readyState == 4) {
adamc@612 137 var isok = false;
adamc@612 138
adamc@612 139 try {
adamc@612 140 if (xhr.status == 200)
adamc@612 141 isok = true;
adamc@612 142 } catch (e) { }
adamc@612 143
adamc@612 144 if (isok)
adamc@613 145 k(parse(xhr.responseText));
adamc@612 146 else
adamc@612 147 alert("Error querying remote server!");
adamc@612 148 }
adamc@609 149 };
adamc@609 150
adamc@609 151 xhr.open("GET", uri, true);
adamc@609 152 xhr.send(null);
adamc@609 153 }