annotate lib/js/urweb.js @ 689:b6a8425e1b1f

Make sure only one pull request runs at a time for each client
author Adam Chlipala <adamc@hcoop.net>
date Thu, 02 Apr 2009 13:48:59 -0400
parents 3b46548f701b
children 01b6f2ee2ef0
rev   line source
adamc@580 1 function cons(v, ls) {
adamc@580 2 return { n : ls, v : v };
adamc@580 3 }
adamc@670 4
adamc@579 5 function callAll(ls) {
adamc@585 6 for (; ls; ls = ls.n)
adamc@579 7 ls.v();
adamc@579 8 }
adamc@574 9
adamc@580 10 function sc(v) {
adamc@580 11 return {v : v, h : null};
adamc@580 12 }
adamc@580 13 function sv(s, v) {
adamc@580 14 s.v = v;
adamc@580 15 callAll(s.h);
adamc@580 16 }
adamc@601 17 function sg(s) {
adamc@601 18 return s.v;
adamc@601 19 }
adamc@579 20
adamc@580 21 function ss(s) {
adamc@580 22 return s;
adamc@580 23 }
adamc@580 24 function sr(v) {
adamc@580 25 return {v : v, h : null};
adamc@580 26 }
adamc@580 27 function sb(x,y) {
adamc@580 28 var z = y(x.v);
adamc@580 29 var s = {v : z.v, h : null};
adamc@580 30
adamc@580 31 function reZ() {
adamc@580 32 z.h = cons(function() { s.v = z.v; callAll(s.h); }, z.h);
adamc@580 33 }
adamc@580 34
adamc@580 35 x.h = cons(function() { z = y(x.v); reZ(); s.v = z.v; callAll(s.h); }, x.h);
adamc@580 36 reZ();
adamc@580 37
adamc@580 38 return s;
adamc@580 39 }
adamc@571 40
adamc@604 41 function lastParent() {
adamc@604 42 var pos = document;
adamc@604 43
adamc@600 44 while (pos.lastChild && pos.lastChild.nodeType == 1)
adamc@600 45 pos = pos.lastChild;
adamc@600 46
adamc@600 47 return pos.parentNode;
adamc@600 48 }
adamc@600 49
adamc@604 50 var thisScript = null;
adamc@603 51
adamc@604 52 function addNode(node) {
adamc@604 53 if (thisScript) {
adamc@604 54 thisScript.parentNode.appendChild(node);
adamc@604 55 thisScript.parentNode.removeChild(thisScript);
adamc@604 56 } else
adamc@604 57 lastParent().appendChild(node);
adamc@603 58 }
adamc@603 59
adamc@604 60 function runScripts(node) {
adamc@604 61 var savedScript = thisScript;
adamc@603 62
adamc@646 63 var scripts = node.getElementsByTagName("script"), scriptsCopy = {};
adamc@604 64 var len = scripts.length;
adamc@646 65 for (var i = 0; i < len; ++i)
adamc@646 66 scriptsCopy[i] = scripts[i];
adamc@604 67 for (var i = 0; i < len; ++i) {
adamc@646 68 thisScript = scriptsCopy[i];
adamc@604 69 eval(thisScript.textContent);
adamc@604 70 }
adamc@604 71
adamc@604 72 thisScript = savedScript;
adamc@603 73 }
adamc@603 74
adamc@603 75 function populate(node, html) {
adamc@603 76 node.innerHTML = html;
adamc@604 77 runScripts(node);
adamc@603 78 }
adamc@603 79
adamc@571 80 function dyn(s) {
adamc@571 81 var x = document.createElement("span");
adamc@604 82 populate(x, s.v);
adamc@604 83 addNode(x);
adamc@603 84 s.h = cons(function() { populate(x, s.v) }, s.h);
adamc@571 85 }
adamc@582 86
adamc@598 87 function inp(t, s) {
adamc@598 88 var x = document.createElement(t);
adamc@598 89 x.value = s.v;
adamc@604 90 addNode(x);
adamc@686 91 s.h = cons(function() { if (x.value != s.v) x.value = s.v }, s.h);
adamc@598 92 x.onkeyup = function() { sv(s, x.value) };
adamc@606 93 return x;
adamc@598 94 }
adamc@598 95
adamc@597 96 function eh(x) {
adamc@597 97 return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
adamc@597 98 }
adamc@597 99
adamc@582 100 function ts(x) { return x.toString() }
adamc@586 101 function bs(b) { return (b ? "True" : "False") }
adamc@586 102
adamc@649 103 function pi(s) {
adamc@649 104 var r = parseInt(s);
adamc@649 105 if (r.toString() == s)
adamc@649 106 return r;
adamc@649 107 else
adamc@649 108 throw "Can't parse int: " + s;
adamc@649 109 }
adamc@649 110
adamc@649 111 function pfl(s) {
adamc@649 112 var r = parseFloat(s);
adamc@649 113 if (r.toString() == s)
adamc@649 114 return r;
adamc@649 115 else
adamc@649 116 throw "Can't parse float: " + s;
adamc@649 117 }
adamc@649 118
adamc@669 119 function whine(msg) {
adamc@669 120 alert(msg);
adamc@669 121 throw msg;
adamc@669 122 }
adamc@669 123
adamc@649 124 function pf() {
adamc@669 125 whine("Pattern match failure");
adamc@649 126 }
adamc@589 127
adamc@603 128 var closures = [];
adamc@603 129
adamc@603 130 function ca(f) {
adamc@603 131 var n = closures.length;
adamc@603 132 closures[n] = f;
adamc@603 133 return n;
adamc@603 134 }
adamc@603 135
adamc@603 136 function cr(n) {
adamc@603 137 return closures[n]();
adamc@603 138 }
adamc@603 139
adamc@609 140
adamc@668 141 var client_id = 0;
adamc@668 142 var client_pass = 0;
adamc@668 143 var url_prefix = "/";
adamc@673 144 var timeout = 60;
adamc@668 145
adamc@668 146 function getXHR(uri)
adamc@609 147 {
adamc@609 148 try {
adamc@609 149 return new XMLHttpRequest();
adamc@609 150 } catch (e) {
adamc@609 151 try {
adamc@609 152 return new ActiveXObject("Msxml2.XMLHTTP");
adamc@609 153 } catch (e) {
adamc@609 154 try {
adamc@609 155 return new ActiveXObject("Microsoft.XMLHTTP");
adamc@609 156 } catch (e) {
adamc@609 157 throw "Your browser doesn't seem to support AJAX.";
adamc@609 158 }
adamc@609 159 }
adamc@609 160 }
adamc@609 161 }
adamc@609 162
adamc@668 163 function requestUri(xhr, uri) {
adamc@668 164 xhr.open("GET", uri, true);
adamc@668 165
adamc@668 166 if (client_id != 0) {
adamc@668 167 xhr.setRequestHeader("UrWeb-Client", client_id.toString());
adamc@668 168 xhr.setRequestHeader("UrWeb-Pass", client_pass.toString());
adamc@668 169 }
adamc@668 170
adamc@668 171 xhr.send(null);
adamc@668 172 }
adamc@668 173
adamc@613 174 function rc(uri, parse, k) {
adamc@609 175 var xhr = getXHR();
adamc@609 176
adamc@609 177 xhr.onreadystatechange = function() {
adamc@612 178 if (xhr.readyState == 4) {
adamc@612 179 var isok = false;
adamc@612 180
adamc@612 181 try {
adamc@612 182 if (xhr.status == 200)
adamc@612 183 isok = true;
adamc@612 184 } catch (e) { }
adamc@612 185
adamc@612 186 if (isok)
adamc@613 187 k(parse(xhr.responseText));
adamc@649 188 else {
adamc@669 189 whine("Error querying remote server!");
adamc@649 190 }
adamc@612 191 }
adamc@609 192 };
adamc@609 193
adamc@668 194 requestUri(xhr, uri);
adamc@609 195 }
adamc@667 196
adamc@667 197 function path_join(s1, s2) {
adamc@667 198 if (s1.length > 0 && s1[s1.length-1] == '/')
adamc@667 199 return s1 + s2;
adamc@667 200 else
adamc@667 201 return s1 + "/" + s2;
adamc@667 202 }
adamc@667 203
adamc@670 204 var channels = [];
adamc@670 205
adamc@670 206 function newQueue() {
adamc@670 207 return { front : null, back : null };
adamc@670 208 }
adamc@670 209 function enqueue(q, v) {
adamc@670 210 if (q.front == null) {
adamc@670 211 q.front = cons(v, null);
adamc@670 212 q.back = q.front;
adamc@670 213 } else {
adamc@670 214 var node = cons(v, null);
adamc@670 215 q.back.n = node;
adamc@670 216 q.back = node;
adamc@670 217 }
adamc@670 218 }
adamc@670 219 function dequeue(q) {
adamc@670 220 if (q.front == null)
adamc@670 221 return null;
adamc@670 222 else {
adamc@670 223 var r = q.front.v;
adamc@670 224 q.front = q.front.n;
adamc@670 225 if (q.front == null)
adamc@670 226 q.back = null;
adamc@670 227 return r;
adamc@670 228 }
adamc@670 229 }
adamc@670 230
adamc@670 231 function newChannel() {
adamc@670 232 return { msgs : newQueue(), listeners : newQueue() };
adamc@670 233 }
adamc@670 234
adamc@667 235 function listener() {
adamc@668 236 var uri = path_join(url_prefix, ".msgs");
adamc@667 237 var xhr = getXHR();
adamc@673 238 var tid, orsc, onTimeout;
adamc@673 239
adamc@673 240 var connect = function () {
adamc@673 241 xhr.onreadystatechange = orsc;
adamc@673 242 tid = window.setTimeout(onTimeout, timeout * 500);
adamc@673 243 requestUri(xhr, uri);
adamc@673 244 }
adamc@673 245
adamc@673 246 orsc = function() {
adamc@667 247 if (xhr.readyState == 4) {
adamc@673 248 window.clearTimeout(tid);
adamc@673 249
adamc@667 250 var isok = false;
adamc@667 251
adamc@667 252 try {
adamc@667 253 if (xhr.status == 200)
adamc@667 254 isok = true;
adamc@667 255 } catch (e) { }
adamc@667 256
adamc@668 257 if (isok) {
adamc@669 258 var lines = xhr.responseText.split("\n");
adamc@669 259 if (lines.length < 2)
adamc@679 260 return; //throw "Empty message from remote server";
adamc@669 261
adamc@669 262 for (var i = 0; i+1 < lines.length; i += 2) {
adamc@670 263 var chn = lines[i];
adamc@670 264 var msg = lines[i+1];
adamc@670 265
adamc@670 266 if (chn < 0)
adamc@670 267 whine("Out-of-bounds channel in message from remote server");
adamc@670 268
adamc@670 269 var ch;
adamc@670 270
adamc@670 271 if (chn >= channels.length || channels[chn] == null) {
adamc@670 272 ch = newChannel();
adamc@670 273 channels[chn] = ch;
adamc@670 274 } else
adamc@670 275 ch = channels[chn];
adamc@670 276
adamc@670 277 var listener = dequeue(ch.listeners);
adamc@670 278 if (listener == null) {
adamc@670 279 enqueue(ch.msgs, msg);
adamc@670 280 } else {
adamc@670 281 listener(msg);
adamc@670 282 }
adamc@669 283 }
adamc@669 284
adamc@673 285 connect();
adamc@668 286 }
adamc@667 287 else {
adamc@679 288 /*try {
adamc@672 289 whine("Error querying remote server for messages! " + xhr.status);
adamc@679 290 } catch (e) { }*/
adamc@667 291 }
adamc@667 292 }
adamc@667 293 };
adamc@667 294
adamc@673 295 onTimeout = function() {
adamc@673 296 xhr.abort();
adamc@673 297 connect();
adamc@673 298 };
adamc@673 299
adamc@673 300 connect();
adamc@667 301 }
adamc@670 302
adamc@670 303 function rv(chn, parse, k) {
adamc@682 304 if (chn == null)
adamc@682 305 return;
adamc@682 306
adamc@670 307 if (chn < 0)
adamc@670 308 whine("Out-of-bounds channel receive");
adamc@670 309
adamc@670 310 var ch;
adamc@670 311
adamc@670 312 if (chn >= channels.length || channels[chn] == null) {
adamc@670 313 ch = newChannel();
adamc@670 314 channels[chn] = ch;
adamc@670 315 } else
adamc@670 316 ch = channels[chn];
adamc@670 317
adamc@670 318 var msg = dequeue(ch.msgs);
adamc@670 319 if (msg == null) {
adamc@670 320 enqueue(ch.listeners, function(msg) { k(parse(msg))(null); });
adamc@670 321 } else {
adamc@670 322 k(parse(msg))(null);
adamc@670 323 }
adamc@670 324 }
adamc@670 325
adamc@679 326 function uf(s) {
adamc@679 327 return escape(s).replace(new RegExp ("/", "g"), "%2F");
adamc@670 328 }
adamc@679 329
adamc@679 330 function uu(s) {
adamc@679 331 return unescape(s).replace(new RegExp ("\\+", "g"), " ");
adamc@679 332 }