1 files changed, 12 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 04c1cfae..8890c446 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -228,6 +228,18 @@ function addNode(node) {
     lastParent().appendChild(node);
 }
 
+function setHTML(html) {
+  var x = document.createElement("span");
+  x.dead = false;
+  x.signal = null;
+  x.sources = null;
+  x.closures = null;
+  x.innerHTML = html;
+  addNode(x);
+  runScripts(x);
+  alert("HTML:\n" + html);
+}  
+
 var thisScript = null;
 
 function runScripts(node) {