Mercurial > urweb

annotate lib/js/urweb.js @ 691:cc58941da3e2

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