comparison 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
comparison
equal deleted inserted replaced
1446:36f7d1debb37 1447:17393c5e2b90
815 if (xhr.status == 200) 815 if (xhr.status == 200)
816 isok = true; 816 isok = true;
817 } catch (e) { } 817 } catch (e) { }
818 818
819 if (isok) { 819 if (isok) {
820 var text = xhr.responseText 820 var text = xhr.responseText;
821 if (text == "") 821 if (text == "")
822 return; 822 return;
823 var lines = text.split("\n"); 823 var lines = text.split("\n");
824 824
825 if (lines.length < 2) { 825 if (lines.length < 2) {
826 discon(); 826 discon();
827 return; 827 return;
828 } 828 }
829 829
830 for (var i = 0; i+1 < lines.length; i += 2) { 830 var messageReader = function(i) {
831 var chn = lines[i]; 831 if (i+1 >= lines.length) {
832 var msg = lines[i+1]; 832 xhrFinished(xhr);
833 833 connect();
834 if (chn < 0) 834 }
835 whine("Out-of-bounds channel in message from remote server"); 835 else {
836 836 var chn = lines[i];
837 var ch; 837 var msg = lines[i+1];
838 838
839 if (chn >= channels.length || channels[chn] == null) { 839 if (chn == "E") {
840 ch = newChannel(); 840 eval(msg);
841 channels[chn] = ch; 841 window.setTimeout(function() { messageReader(i+2); }, 0);
842 } else 842 } else {
843 ch = channels[chn]; 843 if (chn < 0)
844 844 whine("Out-of-bounds channel in message from remote server");
845 var listener = dequeue(ch.listeners); 845
846 if (listener == null) { 846 var ch;
847 enqueue(ch.msgs, msg); 847
848 } else { 848 if (chn >= channels.length || channels[chn] == null) {
849 try { 849 ch = newChannel();
850 listener(msg); 850 channels[chn] = ch;
851 } catch (v) { 851 } else
852 doExn(v); 852 ch = channels[chn];
853
854 var listener = dequeue(ch.listeners);
855 if (listener == null) {
856 enqueue(ch.msgs, msg);
857 } else {
858 try {
859 listener(msg);
860 } catch (v) {
861 doExn(v);
862 }
863 }
864
865 messageReader(i+2);
853 } 866 }
854 } 867 }
855 } 868 }
856 869
857 xhrFinished(xhr); 870 messageReader(0);
858
859 connect();
860 } 871 }
861 else { 872 else {
862 try { 873 try {
863 if (xhr.status != 0) 874 if (xhr.status != 0)
864 servErr("Error querying remote server for messages: " + xhr.status); 875 servErr("Error querying remote server for messages: " + xhr.status);