diff lib/js/urweb.js @ 1447:17393c5e2b90

Send newly created sources with messages to clients
author Adam Chlipala <adam@chlipala.net>
date Sat, 09 Apr 2011 20:00:52 -0400
parents 36f7d1debb37
children 607657eb2865
line wrap: on
line diff
--- a/lib/js/urweb.js	Sat Apr 09 14:36:47 2011 -0400
+++ b/lib/js/urweb.js	Sat Apr 09 20:00:52 2011 -0400
@@ -817,7 +817,7 @@
             } catch (e) { }
 
             if (isok) {
-                var text = xhr.responseText
+                var text = xhr.responseText;
                 if (text == "")
                     return;
                 var lines = text.split("\n");
@@ -827,36 +827,47 @@
                     return;
                 }
 
-                for (var i = 0; i+1 < lines.length; i += 2) {
-                    var chn = lines[i];
-                    var msg = lines[i+1];
+                var messageReader = function(i) {
+                    if (i+1 >= lines.length) {
+                        xhrFinished(xhr);
+                        connect();
+                    }
+                    else {
+                        var chn = lines[i];
+                        var msg = lines[i+1];
 
-                    if (chn < 0)
-                        whine("Out-of-bounds channel in message from remote server");
+                        if (chn == "E") {
+                            eval(msg);
+                            window.setTimeout(function() { messageReader(i+2); }, 0);
+                        } else {
+                            if (chn < 0)
+                                whine("Out-of-bounds channel in message from remote server");
 
-                    var ch;
+                            var ch;
 
-                    if (chn >= channels.length || channels[chn] == null) {
-                        ch = newChannel();
-                        channels[chn] = ch;
-                    } else
-                        ch = channels[chn];
+                            if (chn >= channels.length || channels[chn] == null) {
+                                ch = newChannel();
+                                channels[chn] = ch;
+                            } else
+                                ch = channels[chn];
 
-                    var listener = dequeue(ch.listeners);
-                    if (listener == null) {
-                        enqueue(ch.msgs, msg);
-                    } else {
-                        try {
-                            listener(msg);
-                        } catch (v) {
-                            doExn(v);
+                            var listener = dequeue(ch.listeners);
+                            if (listener == null) {
+                                enqueue(ch.msgs, msg);
+                            } else {
+                                try {
+                                    listener(msg);
+                                } catch (v) {
+                                    doExn(v);
+                                }
+                            }
+
+                            messageReader(i+2);
                         }
                     }
                 }
 
-                xhrFinished(xhr);
-
-                connect();
+                messageReader(0);
             }
             else {
                 try {