# HG changeset patch
# User wenzelm
# Date 1274382603 -7200
# Node ID 9dfcde68b383060ed69af68d3c0515aaecce5d20
# Parent  39207774a9b74f6efb32d9b5aa554da68e304783
mutate displayed document synchronously in Swing thread, for improved robustness;

diff -r 39207774a9b7 -r 9dfcde68b383 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)