comparison lib/js/urweb.js @ 670:f73913d97a40

Proper recv
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Mar 2009 16:03:45 -0400
parents f68eee90dbcf
children 729e65db2e2f
comparison
equal deleted inserted replaced
669:f68eee90dbcf 670:f73913d97a40
1 function cons(v, ls) { 1 function cons(v, ls) {
2 return { n : ls, v : v }; 2 return { n : ls, v : v };
3 } 3 }
4
4 function callAll(ls) { 5 function callAll(ls) {
5 for (; ls; ls = ls.n) 6 for (; ls; ls = ls.n)
6 ls.v(); 7 ls.v();
7 } 8 }
8 9
190 }; 191 };
191 192
192 requestUri(xhr, uri); 193 requestUri(xhr, uri);
193 } 194 }
194 195
195
196 function path_join(s1, s2) { 196 function path_join(s1, s2) {
197 if (s1.length > 0 && s1[s1.length-1] == '/') 197 if (s1.length > 0 && s1[s1.length-1] == '/')
198 return s1 + s2; 198 return s1 + s2;
199 else 199 else
200 return s1 + "/" + s2; 200 return s1 + "/" + s2;
201 }
202
203 var channels = [];
204
205 function newQueue() {
206 return { front : null, back : null };
207 }
208 function enqueue(q, v) {
209 if (q.front == null) {
210 q.front = cons(v, null);
211 q.back = q.front;
212 } else {
213 var node = cons(v, null);
214 q.back.n = node;
215 q.back = node;
216 }
217 }
218 function dequeue(q) {
219 if (q.front == null)
220 return null;
221 else {
222 var r = q.front.v;
223 q.front = q.front.n;
224 if (q.front == null)
225 q.back = null;
226 return r;
227 }
228 }
229
230 function newChannel() {
231 return { msgs : newQueue(), listeners : newQueue() };
201 } 232 }
202 233
203 function listener() { 234 function listener() {
204 var uri = path_join(url_prefix, ".msgs"); 235 var uri = path_join(url_prefix, ".msgs");
205 var xhr = getXHR(); 236 var xhr = getXHR();
216 var lines = xhr.responseText.split("\n"); 247 var lines = xhr.responseText.split("\n");
217 if (lines.length < 2) 248 if (lines.length < 2)
218 whine("Empty message from remote server"); 249 whine("Empty message from remote server");
219 250
220 for (var i = 0; i+1 < lines.length; i += 2) { 251 for (var i = 0; i+1 < lines.length; i += 2) {
221 alert("Message(" + lines[i] + "): " + lines[i+1]); 252 var chn = lines[i];
253 var msg = lines[i+1];
254
255 if (chn < 0)
256 whine("Out-of-bounds channel in message from remote server");
257
258 var ch;
259
260 if (chn >= channels.length || channels[chn] == null) {
261 ch = newChannel();
262 channels[chn] = ch;
263 } else
264 ch = channels[chn];
265
266 var listener = dequeue(ch.listeners);
267 if (listener == null) {
268 enqueue(ch.msgs, msg);
269 } else {
270 listener(msg);
271 }
222 } 272 }
223 273
224 xhr.onreadystatechange = orsc; 274 xhr.onreadystatechange = orsc;
225 requestUri(xhr, uri); 275 requestUri(xhr, uri);
226 } 276 }
231 }; 281 };
232 282
233 xhr.onreadystatechange = orsc; 283 xhr.onreadystatechange = orsc;
234 requestUri(xhr, uri); 284 requestUri(xhr, uri);
235 } 285 }
286
287 function rv(chn, parse, k) {
288 if (chn < 0)
289 whine("Out-of-bounds channel receive");
290
291 var ch;
292
293 if (chn >= channels.length || channels[chn] == null) {
294 ch = newChannel();
295 channels[chn] = ch;
296 } else
297 ch = channels[chn];
298
299 var msg = dequeue(ch.msgs);
300 if (msg == null) {
301 enqueue(ch.listeners, function(msg) { k(parse(msg))(null); });
302 } else {
303 k(parse(msg))(null);
304 }
305 }
306
307 function unesc(s) {
308 return unescape(s).replace("+", " ");
309 }