comparison 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
comparison
equal deleted inserted replaced
689:b6a8425e1b1f 690:01b6f2ee2ef0
1 function cons(v, ls) { 1 function cons(v, ls) {
2 return { n : ls, v : v }; 2 return { next : ls, data : v };
3 } 3 }
4 4 function concat(ls1, ls2) {
5 function callAll(ls) { 5 return (ls1 ? cons(ls1.data, concat(ls1.next, ls2)) : ls2);
6 for (; ls; ls = ls.n) 6 }
7 ls.v(); 7 function member(x, ls) {
8 for (; ls; ls = ls.next)
9 if (ls.data == x)
10 return true;
11 return false;
12 }
13 function remove(x, ls) {
14 return (ls ? (ls.data == x ? ls.next : cons(ls.data, remove(x, ls.next))) : null);
15 }
16 function union(ls1, ls2) {
17 return (ls1 ? (member(ls1.data, ls2) ? union(ls1.next, ls2) : cons(ls1.data, union(ls1.next, ls2))) : ls2);
18 }
19
20
21 function populate(node) {
22 var s = node.signal;
23 var oldSources = node.sources;
24 var sr = s();
25 var newSources = sr.sources;
26
27 for (var sp = oldSources; sp; sp = sp.next)
28 if (!member(sp.data, newSources))
29 sp.data.dyns = remove(node, sp.data.dyns);
30
31 for (var sp = newSources; sp; sp = sp.next)
32 if (!member(sp.data, oldSources))
33 sp.data.dyns = cons(node, sp.data.dyns);
34
35 node.sources = newSources;
36 node.recreate(sr.data);
8 } 37 }
9 38
10 function sc(v) { 39 function sc(v) {
11 return {v : v, h : null}; 40 return {data : v, dyns : null};
12 } 41 }
13 function sv(s, v) { 42 function sv(s, v) {
14 s.v = v; 43 s.data = v;
15 callAll(s.h); 44 for (var ls = s.dyns; ls; ls = ls.next)
45 if (!ls.dead)
46 populate(ls.data);
16 } 47 }
17 function sg(s) { 48 function sg(s) {
18 return s.v; 49 return s.data;
19 } 50 }
20 51
21 function ss(s) { 52 function ss(s) {
22 return s; 53 return function() { return {sources : cons(s, null), data : s.data } };
23 } 54 }
24 function sr(v) { 55 function sr(v) {
25 return {v : v, h : null}; 56 return function() { return {sources : null, data : v } };
26 } 57 }
27 function sb(x,y) { 58 function sb(x,y) {
28 var z = y(x.v); 59 return function() {
29 var s = {v : z.v, h : null}; 60 var xr = x();
30 61 var yr = y(xr.data)();
31 function reZ() { 62 return {sources : union(xr.sources, yr.sources), data : yr.data};
32 z.h = cons(function() { s.v = z.v; callAll(s.h); }, z.h); 63 };
33 }
34
35 x.h = cons(function() { z = y(x.v); reZ(); s.v = z.v; callAll(s.h); }, x.h);
36 reZ();
37
38 return s;
39 } 64 }
40 65
41 function lastParent() { 66 function lastParent() {
42 var pos = document; 67 var pos = document;
43 68
44 while (pos.lastChild && pos.lastChild.nodeType == 1) 69 while (pos.lastChild && pos.lastChild.nodeType == 1)
45 pos = pos.lastChild; 70 pos = pos.lastChild;
46 71
47 return pos.parentNode; 72 return pos.parentNode;
48 } 73 }
49
50 var thisScript = null;
51 74
52 function addNode(node) { 75 function addNode(node) {
53 if (thisScript) { 76 if (thisScript) {
54 thisScript.parentNode.appendChild(node); 77 thisScript.parentNode.appendChild(node);
55 thisScript.parentNode.removeChild(thisScript); 78 thisScript.parentNode.removeChild(thisScript);
56 } else 79 } else
57 lastParent().appendChild(node); 80 lastParent().appendChild(node);
58 } 81 }
82
83 var thisScript = null;
59 84
60 function runScripts(node) { 85 function runScripts(node) {
61 var savedScript = thisScript; 86 var savedScript = thisScript;
62 87
63 var scripts = node.getElementsByTagName("script"), scriptsCopy = {}; 88 var scripts = node.getElementsByTagName("script"), scriptsCopy = {};
70 } 95 }
71 96
72 thisScript = savedScript; 97 thisScript = savedScript;
73 } 98 }
74 99
75 function populate(node, html) {
76 node.innerHTML = html;
77 runScripts(node);
78 }
79 100
80 function dyn(s) { 101 function dyn(s) {
81 var x = document.createElement("span"); 102 var x = document.createElement("span");
82 populate(x, s.v); 103 x.dead = false;
104 x.signal = s;
105 x.sources = null;
106 x.recreate = function(v) {
107 var spans = x.getElementsByTagName("span");
108 for (var i = 0; i < spans.length; ++i) {
109 var span = spans[i];
110 span.dead = true;
111 for (var ls = span.sources; ls; ls = ls.next)
112 ls.data.dyns = remove(span, ls.data.dyns);
113 }
114
115 x.innerHTML = v;
116 runScripts(x);
117 };
118 populate(x);
83 addNode(x); 119 addNode(x);
84 s.h = cons(function() { populate(x, s.v) }, s.h);
85 } 120 }
86 121
87 function inp(t, s) { 122 function inp(t, s) {
88 var x = document.createElement(t); 123 var x = document.createElement(t);
89 x.value = s.v; 124 x.dead = false;
125 x.signal = ss(s);
126 x.sources = null;
127 x.recreate = function(v) { if (x.value != v) x.value = v; };
128 populate(x);
90 addNode(x); 129 addNode(x);
91 s.h = cons(function() { if (x.value != s.v) x.value = s.v }, s.h);
92 x.onkeyup = function() { sv(s, x.value) }; 130 x.onkeyup = function() { sv(s, x.value) };
93 return x; 131 return x;
94 } 132 }
95 133
96 function eh(x) { 134 function eh(x) {
210 if (q.front == null) { 248 if (q.front == null) {
211 q.front = cons(v, null); 249 q.front = cons(v, null);
212 q.back = q.front; 250 q.back = q.front;
213 } else { 251 } else {
214 var node = cons(v, null); 252 var node = cons(v, null);
215 q.back.n = node; 253 q.back.next = node;
216 q.back = node; 254 q.back = node;
217 } 255 }
218 } 256 }
219 function dequeue(q) { 257 function dequeue(q) {
220 if (q.front == null) 258 if (q.front == null)
221 return null; 259 return null;
222 else { 260 else {
223 var r = q.front.v; 261 var r = q.front.data;
224 q.front = q.front.n; 262 q.front = q.front.next;
225 if (q.front == null) 263 if (q.front == null)
226 q.back = null; 264 q.back = null;
227 return r; 265 return r;
228 } 266 }
229 } 267 }
255 } catch (e) { } 293 } catch (e) { }
256 294
257 if (isok) { 295 if (isok) {
258 var lines = xhr.responseText.split("\n"); 296 var lines = xhr.responseText.split("\n");
259 if (lines.length < 2) 297 if (lines.length < 2)
260 return; //throw "Empty message from remote server"; 298 return; // throw "Empty message from remote server";
261 299
262 for (var i = 0; i+1 < lines.length; i += 2) { 300 for (var i = 0; i+1 < lines.length; i += 2) {
263 var chn = lines[i]; 301 var chn = lines[i];
264 var msg = lines[i+1]; 302 var msg = lines[i+1];
265 303
322 k(parse(msg))(null); 360 k(parse(msg))(null);
323 } 361 }
324 } 362 }
325 363
326 function uf(s) { 364 function uf(s) {
327 return escape(s).replace(new RegExp ("/", "g"), "%2F"); 365 return escape(s).replace(new RegExp ("/", "g"), "%2F");
328 } 366 }
329 367
330 function uu(s) { 368 function uu(s) {
331 return unescape(s).replace(new RegExp ("\\+", "g"), " "); 369 return unescape(s).replace(new RegExp ("\\+", "g"), " ");
332 } 370 }