mutate displayed document synchronously in Swing thread, for improved robustness;
--- 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)