changeset 1802:e3ec868567ce

Undo change to script evaluation, originally made to support <active> + 'giveFocus'; alternate approach to making 'giveFocus' work in dynamic code generatione
author Adam Chlipala <adam@chlipala.net>
date Fri, 03 Aug 2012 08:38:47 -0400
parents 5c51ae0d643b
children d2383ffc18ab
files lib/js/urweb.js
diffstat 1 files changed, 10 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/lib/js/urweb.js	Fri Aug 03 08:32:03 2012 -0400
+++ b/lib/js/urweb.js	Fri Aug 03 08:38:47 2012 -0400
@@ -815,6 +815,7 @@
 
             var dummy = document.createElement("body");
             dummy.innerHTML = "<table>" + html + "</table>";
+            runScripts(dummy);
             var table = x.parentNode;
 
             if (table) {
@@ -842,12 +843,12 @@
                 for (var node = tbody.firstChild; node; node = next) {
                     next = node.nextSibling;
                     table.insertBefore(node, x);
-                    runScripts(node);
                 }
             }
         } else if (pnode == "tr") {
             var dummy = document.createElement("body");
             dummy.innerHTML = "<table><tr>" + html + "</tr></table>";
+            runScripts(dummy);
             var table = x.parentNode;
 
             if (table) {
@@ -865,15 +866,14 @@
                 for (var node = tr.firstChild; node; node = next) {
                     next = node.nextSibling;
                     table.insertBefore(node, x);
-                    runScripts(node);
                 }
             }
         } else {
             firstChild = document.createElement("span");
             firstChild.innerHTML = html;
+            runScripts(firstChild);
             if (x.parentNode)
                 x.parentNode.insertBefore(firstChild, x);
-            runScripts(firstChild);
         }
     };
 
@@ -1863,12 +1863,14 @@
 }
 
 function giveFocus(id) {
-    var node = document.getElementById(id);
+    window.setTimeout(function() {
+        var node = document.getElementById(id);
 
-    if (node)
-        node.focus();
-    else
-        er("Tried to give focus to ID not used in document: " + id);
+        if (node)
+            node.focus();
+        else
+            er("Tried to give focus to ID not used in document: " + id);
+    }, 0);
 }