diff lib/js/urweb.js @ 728:2197f0e24a9f

Avoid thread death via message receive
author Adam Chlipala <adamc@hcoop.net>
date Thu, 16 Apr 2009 13:00:40 -0400
parents 6fc633d990e7
children 7c6b6c3c7b79
line wrap: on
line diff
--- a/lib/js/urweb.js	Thu Apr 16 12:43:55 2009 -0400
+++ b/lib/js/urweb.js	Thu Apr 16 13:00:40 2009 -0400
@@ -75,6 +75,14 @@
     return tr;
 }
 
+function flattenLocal(s) {
+  var cls = {v : null};
+  var r = flatten(cls, s);
+  for (cl = cls.v; cl != null; cl = cl.next)
+    freeClosure(cl.data);
+  return r;
+}
+
 
 
 // Dynamic tree management
@@ -259,7 +267,21 @@
 function er(s) {
   for (var ls = errorHandlers; ls; ls = ls.next)
     ls.data(s)(null);
-  throw s;
+  throw {uw_error: s};
+}
+
+var failHandlers = null;
+
+function onFail(f) {
+  failHandlers = cons(f, failHandlers);
+}
+
+function doExn(v) {
+  if (v == null || v.uw_error == null) {
+    var s = (v == null ? "null" : v.toString());
+    for (var ls = failHandlers; ls; ls = ls.next)
+      ls.data(s)(null);
+  }
 }
 
 
@@ -299,11 +321,7 @@
 }
 
 function rc(uri, parse, k) {
-  var cls = {v : null};
-  uri = flatten(cls, uri);
-  for (cl = cls.v; cl != null; cl = cl.next)
-    freeClosure(cl.data);
-
+  uri = flattenLocal(uri);
   var xhr = getXHR();
 
   xhr.onreadystatechange = function() {
@@ -410,7 +428,11 @@
           if (listener == null) {
             enqueue(ch.msgs, msg);
           } else {
-            listener(msg);
+            try {
+              listener(msg);
+            } catch (v) {
+              doExn(v);
+            }
           }
         }
 
@@ -451,7 +473,11 @@
   if (msg == null) {
     enqueue(ch.listeners, function(msg) { k(parse(msg))(null); });
   } else {
-    k(parse(msg))(null);
+    try {
+      k(parse(msg))(null);
+    } catch (v) {
+      doExn(v);
+    }
   }
 }