diff lib/js/urweb.js @ 1803:d2383ffc18ab

Back out last change and pursue a different fix, based on explicitly aborting script execution at times when we don't expect scripts to run
author Adam Chlipala <adam@chlipala.net>
date Fri, 03 Aug 2012 12:39:04 -0400
parents e3ec868567ce
children 9913c81bdbef
line wrap: on
line diff
--- a/lib/js/urweb.js	Fri Aug 03 08:38:47 2012 -0400
+++ b/lib/js/urweb.js	Fri Aug 03 12:39:04 2012 -0400
@@ -691,6 +691,8 @@
     return pos;
 }
 
+var thisScript = null;
+
 function parent() {
     return thisScript ? thisScript.parentNode : lastParent();
 }
@@ -703,10 +705,21 @@
         lastParent().appendChild(node);
 }
 
-var thisScript = null;
+function runScripts(node) {
+    if (node.tagName == "SCRIPT") {
+        var savedScript = thisScript;
+        thisScript = node;
+        
+        try {
+            eval(thisScript.text);
+        } catch (v) {
+            doExn(v);
+        }
+        if (thisScript.parentNode)
+            thisScript.parentNode.removeChild(thisScript);
 
-function runScripts(node) {
-    if (node.getElementsByTagName) {
+        thisScript = savedScript;
+    } else if (node.getElementsByTagName) {
         var savedScript = thisScript;
 
         var scripts = node.getElementsByTagName("script"), scriptsCopy = [];
@@ -747,7 +760,7 @@
 
     var script, next;
 
-    while (table.tagName != "TABLE")
+    while (table && table.tagName != "TABLE")
         table = table.parentNode;
 
     for (var tbody = table.firstChild; tbody; tbody = tbody.nextSibling) {
@@ -776,7 +789,12 @@
     table.appendChild(tbody);
 }
 
+var suspendScripts = false;
+
 function dyn(pnode, s) {
+    if (suspendScripts)
+        return;
+
     var x = document.createElement("script");
     x.dead = false;
     x.signal = s;
@@ -814,8 +832,14 @@
             normalizeTable(x.parentNode);
 
             var dummy = document.createElement("body");
-            dummy.innerHTML = "<table>" + html + "</table>";
-            runScripts(dummy);
+            suspendScripts = true;
+            try {
+                dummy.innerHTML = "<table>" + html + "</table>";
+            } catch (e) {
+                suspendScripts = false;
+                throw e;
+            }
+
             var table = x.parentNode;
 
             if (table) {
@@ -843,12 +867,23 @@
                 for (var node = tbody.firstChild; node; node = next) {
                     next = node.nextSibling;
                     table.insertBefore(node, x);
+                    suspendScripts = false;
+                    runScripts(node);
+                    suspendScripts = true;
                 }
             }
+
+            suspendScripts = false;
         } else if (pnode == "tr") {
             var dummy = document.createElement("body");
-            dummy.innerHTML = "<table><tr>" + html + "</tr></table>";
-            runScripts(dummy);
+            suspendScripts = true;
+            try {
+                dummy.innerHTML = "<table><tr>" + html + "</tr></table>";
+            } catch (e) {
+                suspendScripts = false;
+                throw e;
+            }
+
             var table = x.parentNode;
 
             if (table) {
@@ -866,14 +901,27 @@
                 for (var node = tr.firstChild; node; node = next) {
                     next = node.nextSibling;
                     table.insertBefore(node, x);
+                    suspendScripts = false;
+                    runScripts(node);
+                    suspendScripts = true;
                 }
-            }
+            };
+
+            suspendScripts = false;
         } else {
             firstChild = document.createElement("span");
-            firstChild.innerHTML = html;
+
+            suspendScripts = true;
+            try {
+                firstChild.innerHTML = html;
+                if (x.parentNode)
+                    x.parentNode.insertBefore(firstChild, x);
+            } catch (e) {
+                suspendScripts = false;
+                throw e;
+            }
+            suspendScripts = false;
             runScripts(firstChild);
-            if (x.parentNode)
-                x.parentNode.insertBefore(firstChild, x);
         }
     };
 
@@ -909,13 +957,18 @@
     var cls = {v : null};
     var html = flatten(cls, html);
     x.closures = cls.v;
+    suspendScripts = true;
     node.innerHTML = html;
+    suspendScripts = false;
     runScripts(node);
 }
 
 var maySuspend = true;
 
 function active(s) {
+    if (suspendScripts)
+        return;
+
     var span = document.createElement("span");
     addNode(span);
     var ms = maySuspend;
@@ -944,6 +997,9 @@
 }
 
 function inp(s, name) {
+    if (suspendScripts)
+        return;
+
     var x = input(document.createElement("input"), s,
                   function(x) { return function(v) { if (x.value != v) x.value = v; }; }, null, name);
     x.value = s.data;
@@ -969,6 +1025,9 @@
 }
 
 function sel(s, content) {
+    if (suspendScripts)
+        return;
+
     var dummy = document.createElement("span");
     dummy.innerHTML = "<select>" + content + "</select>";
     var x = input(dummy.firstChild, s, function(x) { return function(v) { if (selectValue(x) != v) setSelectValue(x, v); }; });
@@ -989,6 +1048,9 @@
 }
 
 function chk(s) {
+    if (suspendScripts)
+        return;
+
     var x = input(document.createElement("input"), s,
                   function(x) { return function(v) { if (x.checked != v) x.checked = v; }; }, "checkbox");
     x.defaultChecked = x.checked = s.data;
@@ -998,6 +1060,9 @@
 }
 
 function tbx(s) {
+    if (suspendScripts)
+        return;
+
     var x = input(document.createElement("textarea"), s,
                   function(x) { return function(v) { if (x.value != v) x.value = v; }; });
     x.innerHTML = s.data;
@@ -1007,12 +1072,17 @@
 }
 
 function dynClass(html, s_class, s_style) {
+    if (suspendScripts)
+        return;
+
     var htmlCls = {v : null};
     html = flatten(htmlCls, html);
     htmlCls = htmlCls.v;
 
     var dummy = document.createElement("body");
+    suspendScripts = true;
     dummy.innerHTML = html;
+    suspendScripts = false;
     var html = dummy.firstChild;
     dummy.removeChild(html);
     addNode(html);
@@ -1863,14 +1933,12 @@
 }
 
 function giveFocus(id) {
-    window.setTimeout(function() {
-        var node = document.getElementById(id);
+    var node = document.getElementById(id);
 
-        if (node)
-            node.focus();
-        else
-            er("Tried to give focus to ID not used in document: " + id);
-    }, 0);
+    if (node)
+        node.focus();
+    else
+        er("Tried to give focus to ID not used in document: " + id);
 }