# HG changeset patch # User Adam Chlipala # Date 1242511754 14400 # Node ID 2fbd1ac2f04b07ba0b07272dd110ebc45765dfc3 # Parent 50b4825115f01edc5db23780e0a30a9b04071ce3 Loading an FCKeditor diff -r 50b4825115f0 -r 2fbd1ac2f04b lib/js/urweb.js --- a/lib/js/urweb.js Sat May 16 16:59:24 2009 -0400 +++ b/lib/js/urweb.js Sat May 16 18:09:14 2009 -0400 @@ -228,6 +228,18 @@ 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) { diff -r 50b4825115f0 -r 2fbd1ac2f04b src/cjr_print.sml --- a/src/cjr_print.sml Sat May 16 16:59:24 2009 -0400 +++ b/src/cjr_print.sml Sat May 16 18:09:14 2009 -0400 @@ -2841,14 +2841,22 @@ string "uw_write(ctx, begin_xhtml);", newline, string "uw_set_script_header(ctx, \"", - string (case side of + let + val scripts = + case side of ServerOnly => "" | _ => "\\n"), - p_list (fn x => string ("")) - (Settings.getScripts ()), + ^ "\\\">\\n" + + val scripts = foldl (fn (x, scripts) => + scripts + ^ "\\n") + scripts (Settings.getScripts ()) + in + string scripts + end, string "\");", newline, string "uw_set_needs_push(ctx, ",