annotate lib/js/urweb.js @ 690:01b6f2ee2ef0

Redo signal implementation to avoid memory leaks
author Adam Chlipala <adamc@hcoop.net>
date Thu, 02 Apr 2009 15:12:06 -0400
parents 3b46548f701b
children cc58941da3e2
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@669 157 function whine(msg) {
adamc@669 158 alert(msg);
adamc@669 159 throw msg;
adamc@669 160 }
adamc@669 161
adamc@649 162 function pf() {
adamc@669 163 whine("Pattern match failure");
adamc@649 164 }
adamc@589 165
adamc@603 166 var closures = [];
adamc@603 167
adamc@603 168 function ca(f) {
adamc@603 169 var n = closures.length;
adamc@603 170 closures[n] = f;
adamc@603 171 return n;
adamc@603 172 }
adamc@603 173
adamc@603 174 function cr(n) {
adamc@603 175 return closures[n]();
adamc@603 176 }
adamc@603 177
adamc@609 178
adamc@668 179 var client_id = 0;
adamc@668 180 var client_pass = 0;
adamc@668 181 var url_prefix = "/";
adamc@673 182 var timeout = 60;
adamc@668 183
adamc@668 184 function getXHR(uri)
adamc@609 185 {
adamc@609 186 try {
adamc@609 187 return new XMLHttpRequest();
adamc@609 188 } catch (e) {
adamc@609 189 try {
adamc@609 190 return new ActiveXObject("Msxml2.XMLHTTP");
adamc@609 191 } catch (e) {
adamc@609 192 try {
adamc@609 193 return new ActiveXObject("Microsoft.XMLHTTP");
adamc@609 194 } catch (e) {
adamc@609 195 throw "Your browser doesn't seem to support AJAX.";
adamc@609 196 }
adamc@609 197 }
adamc@609 198 }
adamc@609 199 }
adamc@609 200
adamc@668 201 function requestUri(xhr, uri) {
adamc@668 202 xhr.open("GET", uri, true);
adamc@668 203
adamc@668 204 if (client_id != 0) {
adamc@668 205 xhr.setRequestHeader("UrWeb-Client", client_id.toString());
adamc@668 206 xhr.setRequestHeader("UrWeb-Pass", client_pass.toString());
adamc@668 207 }
adamc@668 208
adamc@668 209 xhr.send(null);
adamc@668 210 }
adamc@668 211
adamc@613 212 function rc(uri, parse, k) {
adamc@609 213 var xhr = getXHR();
adamc@609 214
adamc@609 215 xhr.onreadystatechange = function() {
adamc@612 216 if (xhr.readyState == 4) {
adamc@612 217 var isok = false;
adamc@612 218
adamc@612 219 try {
adamc@612 220 if (xhr.status == 200)
adamc@612 221 isok = true;
adamc@612 222 } catch (e) { }
adamc@612 223
adamc@612 224 if (isok)
adamc@613 225 k(parse(xhr.responseText));
adamc@649 226 else {
adamc@669 227 whine("Error querying remote server!");
adamc@649 228 }
adamc@612 229 }
adamc@609 230 };
adamc@609 231
adamc@668 232 requestUri(xhr, uri);
adamc@609 233 }
adamc@667 234
adamc@667 235 function path_join(s1, s2) {
adamc@667 236 if (s1.length > 0 && s1[s1.length-1] == '/')
adamc@667 237 return s1 + s2;
adamc@667 238 else
adamc@667 239 return s1 + "/" + s2;
adamc@667 240 }
adamc@667 241
adamc@670 242 var channels = [];
adamc@670 243
adamc@670 244 function newQueue() {
adamc@670 245 return { front : null, back : null };
adamc@670 246 }
adamc@670 247 function enqueue(q, v) {
adamc@670 248 if (q.front == null) {
adamc@670 249 q.front = cons(v, null);
adamc@670 250 q.back = q.front;
adamc@670 251 } else {
adamc@670 252 var node = cons(v, null);
adamc@690 253 q.back.next = node;
adamc@670 254 q.back = node;
adamc@670 255 }
adamc@670 256 }
adamc@670 257 function dequeue(q) {
adamc@670 258 if (q.front == null)
adamc@670 259 return null;
adamc@670 260 else {
adamc@690 261 var r = q.front.data;
adamc@690 262 q.front = q.front.next;
adamc@670 263 if (q.front == null)
adamc@670 264 q.back = null;
adamc@670 265 return r;
adamc@670 266 }
adamc@670 267 }
adamc@670 268
adamc@670 269 function newChannel() {
adamc@670 270 return { msgs : newQueue(), listeners : newQueue() };
adamc@670 271 }
adamc@670 272
adamc@667 273 function listener() {
adamc@668 274 var uri = path_join(url_prefix, ".msgs");
adamc@667 275 var xhr = getXHR();
adamc@673 276 var tid, orsc, onTimeout;
adamc@673 277
adamc@673 278 var connect = function () {
adamc@673 279 xhr.onreadystatechange = orsc;
adamc@673 280 tid = window.setTimeout(onTimeout, timeout * 500);
adamc@673 281 requestUri(xhr, uri);
adamc@673 282 }
adamc@673 283
adamc@673 284 orsc = function() {
adamc@667 285 if (xhr.readyState == 4) {
adamc@673 286 window.clearTimeout(tid);
adamc@673 287
adamc@667 288 var isok = false;
adamc@667 289
adamc@667 290 try {
adamc@667 291 if (xhr.status == 200)
adamc@667 292 isok = true;
adamc@667 293 } catch (e) { }
adamc@667 294
adamc@668 295 if (isok) {
adamc@669 296 var lines = xhr.responseText.split("\n");
adamc@669 297 if (lines.length < 2)
adamc@690 298 return; // throw "Empty message from remote server";
adamc@669 299
adamc@669 300 for (var i = 0; i+1 < lines.length; i += 2) {
adamc@670 301 var chn = lines[i];
adamc@670 302 var msg = lines[i+1];
adamc@670 303
adamc@670 304 if (chn < 0)
adamc@670 305 whine("Out-of-bounds channel in message from remote server");
adamc@670 306
adamc@670 307 var ch;
adamc@670 308
adamc@670 309 if (chn >= channels.length || channels[chn] == null) {
adamc@670 310 ch = newChannel();
adamc@670 311 channels[chn] = ch;
adamc@670 312 } else
adamc@670 313 ch = channels[chn];
adamc@670 314
adamc@670 315 var listener = dequeue(ch.listeners);
adamc@670 316 if (listener == null) {
adamc@670 317 enqueue(ch.msgs, msg);
adamc@670 318 } else {
adamc@670 319 listener(msg);
adamc@670 320 }
adamc@669 321 }
adamc@669 322
adamc@673 323 connect();
adamc@668 324 }
adamc@667 325 else {
adamc@679 326 /*try {
adamc@672 327 whine("Error querying remote server for messages! " + xhr.status);
adamc@679 328 } catch (e) { }*/
adamc@667 329 }
adamc@667 330 }
adamc@667 331 };
adamc@667 332
adamc@673 333 onTimeout = function() {
adamc@673 334 xhr.abort();
adamc@673 335 connect();
adamc@673 336 };
adamc@673 337
adamc@673 338 connect();
adamc@667 339 }
adamc@670 340
adamc@670 341 function rv(chn, parse, k) {
adamc@682 342 if (chn == null)
adamc@682 343 return;
adamc@682 344
adamc@670 345 if (chn < 0)
adamc@670 346 whine("Out-of-bounds channel receive");
adamc@670 347
adamc@670 348 var ch;
adamc@670 349
adamc@670 350 if (chn >= channels.length || channels[chn] == null) {
adamc@670 351 ch = newChannel();
adamc@670 352 channels[chn] = ch;
adamc@670 353 } else
adamc@670 354 ch = channels[chn];
adamc@670 355
adamc@670 356 var msg = dequeue(ch.msgs);
adamc@670 357 if (msg == null) {
adamc@670 358 enqueue(ch.listeners, function(msg) { k(parse(msg))(null); });
adamc@670 359 } else {
adamc@670 360 k(parse(msg))(null);
adamc@670 361 }
adamc@670 362 }
adamc@670 363
adamc@679 364 function uf(s) {
adamc@690 365 return escape(s).replace(new RegExp ("/", "g"), "%2F");
adamc@670 366 }
adamc@679 367
adamc@679 368 function uu(s) {
adamc@679 369 return unescape(s).replace(new RegExp ("\\+", "g"), " ");
adamc@679 370 }