mutate displayed document synchronously in Swing thread, for improved robustness;
authorwenzelm
Thu, 20 May 2010 21:10:03 +0200
changeset 37016 9dfcde68b383
parent 37015 39207774a9b7
child 37017 cf6625012282
mutate displayed document synchronously in Swing thread, for improved robustness;
src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 21:07:05 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 21:10:03 2010 +0200
@@ -143,9 +143,11 @@
             .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
 
       val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
-      current_DOM.removeChild(current_DOM.getLastChild())
-      current_DOM.appendChild(node)
-      Swing_Thread.now { setDocument(current_DOM, rcontext) }
+      Swing_Thread.now {
+        current_DOM.removeChild(current_DOM.getLastChild())
+        current_DOM.appendChild(node)
+        setDocument(current_DOM, rcontext)
+      }
     }
 
     resize(initial_font_size)