comparison lib/js/urweb.js @ 703:a5d8b470d7ca

Fixing some regressions and other bugs
author Adam Chlipala <adamc@hcoop.net>
date Sun, 05 Apr 2009 16:17:32 -0400
parents 655bcc9b77e0
children 6fc633d990e7
comparison
equal deleted inserted replaced
702:5b8617b73540 703:a5d8b470d7ca
16 return (ls ? (ls.data == x ? ls.next : cons(ls.data, remove(x, ls.next))) : null); 16 return (ls ? (ls.data == x ? ls.next : cons(ls.data, remove(x, ls.next))) : null);
17 } 17 }
18 function union(ls1, ls2) { 18 function union(ls1, ls2) {
19 return (ls1 ? (member(ls1.data, ls2) ? union(ls1.next, ls2) : cons(ls1.data, union(ls1.next, ls2))) : ls2); 19 return (ls1 ? (member(ls1.data, ls2) ? union(ls1.next, ls2) : cons(ls1.data, union(ls1.next, ls2))) : ls2);
20 } 20 }
21 function length(ls) {
22 return (ls ? 1 + length(ls.next) : 0);
23 }
21 24
22 25
23 // Embedding closures in XML strings 26 // Embedding closures in XML strings
24 27
25 function cs(f) { 28 function cs(f) {
36 else 39 else
37 return s1 + s2; 40 return s1 + s2;
38 } 41 }
39 42
40 var closures = []; 43 var closures = [];
44 var freeClosures = null;
41 45
42 function newClosure(f) { 46 function newClosure(f) {
43 var n = closures.length; 47 var n;
48 if (freeClosures == null) {
49 n = closures.length;
50 } else {
51 n = freeClosures.data;
52 freeClosures = freeClosures.next;
53 }
44 closures[n] = f; 54 closures[n] = f;
45 return n; 55 return n;
46 } 56 }
47 57
58 function freeClosure(n) {
59 closures[n] = null;
60 freeClosures = cons(n, freeClosures);
61 }
62
48 function cr(n) { 63 function cr(n) {
49 return closures[n](); 64 return closures[n]();
50 } 65 }
51 66
52 function flatten(tr) { 67 function flatten(cls, tr) {
53 if (tr.cat1 != null) 68 if (tr.cat1 != null)
54 return flatten(tr.cat1) + flatten(tr.cat2); 69 return flatten(cls, tr.cat1) + flatten(cls, tr.cat2);
55 else if (tr.closure != null) 70 else if (tr.closure != null) {
56 return "cr(" + newClosure(tr.closure) + ")"; 71 var cl = newClosure(tr.closure);
57 else 72 cls.v = cons(cl, cls.v);
73 return "cr(" + cl + ")";
74 } else
58 return tr; 75 return tr;
59 } 76 }
60 77
61 function clearClosures() {
62 closures = [];
63 }
64 78
65 79
66 // Dynamic tree management 80 // Dynamic tree management
67 81
68 function populate(node) { 82 function populate(node) {
152 function dyn(s) { 166 function dyn(s) {
153 var x = document.createElement("span"); 167 var x = document.createElement("span");
154 x.dead = false; 168 x.dead = false;
155 x.signal = s; 169 x.signal = s;
156 x.sources = null; 170 x.sources = null;
171 x.closures = null;
157 x.recreate = function(v) { 172 x.recreate = function(v) {
158 ++dynDepth; 173 for (var ls = x.closures; ls; ls = ls.next)
174 freeClosure(ls.data);
159 175
160 var spans = x.getElementsByTagName("span"); 176 var spans = x.getElementsByTagName("span");
161 for (var i = 0; i < spans.length; ++i) { 177 for (var i = 0; i < spans.length; ++i) {
162 var span = spans[i]; 178 var span = spans[i];
163 span.dead = true; 179 span.dead = true;
164 for (var ls = span.sources; ls; ls = ls.next) 180 for (var ls = span.sources; ls; ls = ls.next)
165 ls.data.dyns = remove(span, ls.data.dyns); 181 ls.data.dyns = remove(span, ls.data.dyns);
182 for (var ls = span.closures; ls; ls = ls.next)
183 freeClosure(ls.data);
166 } 184 }
167 185
168 x.innerHTML = flatten(v); 186 var cls = {v : null};
187 x.innerHTML = flatten(cls, v);
188 x.closures = cls.v;
169 runScripts(x); 189 runScripts(x);
170
171 if (--dynDepth == 0)
172 clearClosures();
173 }; 190 };
191 addNode(x);
174 populate(x); 192 populate(x);
175 addNode(x);
176 } 193 }
177 194
178 function inp(t, s) { 195 function inp(t, s) {
179 var x = document.createElement(t); 196 var x = document.createElement(t);
180 x.dead = false; 197 x.dead = false;
234 } 251 }
235 252
236 253
237 // Remote calls 254 // Remote calls
238 255
239 var client_id = 0; 256 var client_id = null;
240 var client_pass = 0; 257 var client_pass = 0;
241 var url_prefix = "/"; 258 var url_prefix = "/";
242 var timeout = 60; 259 var timeout = 60;
243 260
244 function getXHR(uri) 261 function getXHR(uri)
259 } 276 }
260 277
261 function requestUri(xhr, uri) { 278 function requestUri(xhr, uri) {
262 xhr.open("GET", uri, true); 279 xhr.open("GET", uri, true);
263 280
264 if (client_id != 0) { 281 if (client_id != null) {
265 xhr.setRequestHeader("UrWeb-Client", client_id.toString()); 282 xhr.setRequestHeader("UrWeb-Client", client_id.toString());
266 xhr.setRequestHeader("UrWeb-Pass", client_pass.toString()); 283 xhr.setRequestHeader("UrWeb-Pass", client_pass.toString());
267 } 284 }
268 285
269 xhr.send(null); 286 xhr.send(null);
270 } 287 }
271 288
272 function rc(uri, parse, k) { 289 function rc(uri, parse, k) {
290 var cls = {v : null};
291 uri = flatten(cls, uri);
292 for (cl = cls.v; cl != null; cl = cl.next)
293 freeClosure(cl.data);
294
273 var xhr = getXHR(); 295 var xhr = getXHR();
274 296
275 xhr.onreadystatechange = function() { 297 xhr.onreadystatechange = function() {
276 if (xhr.readyState == 4) { 298 if (xhr.readyState == 4) {
277 var isok = false; 299 var isok = false;