Send newly created sources with messages to clients

1 files changed, 38 insertions, 27 deletions

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index f5764896..5a6ce21f 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -817,7 +817,7 @@ function listener() {
             } catch (e) { }
 
             if (isok) {
-                var text = xhr.responseText
+                var text = xhr.responseText;
                 if (text == "")
                     return;
                 var lines = text.split("\n");
@@ -827,36 +827,47 @@ function listener() {
                     return;
                 }
 
-                for (var i = 0; i+1 < lines.length; i += 2) {
-                    var chn = lines[i];
-                    var msg = lines[i+1];
-
-                    if (chn < 0)
-                        whine("Out-of-bounds channel in message from remote server");
-
-                    var ch;
-
-                    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 messageReader = function(i) {
+                    if (i+1 >= lines.length) {
+                        xhrFinished(xhr);
+                        connect();
+                    }
+                    else {
+                        var chn = lines[i];
+                        var msg = lines[i+1];
+
+                        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;
+
+                            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);
+                                }
+                            }
+
+                            messageReader(i+2);
                         }
                     }
                 }
 
-                xhrFinished(xhr);
-
-                connect();
+                messageReader(0);
             }
             else {
                 try {