1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 21:07:05 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 21:10:03 2010 +0200
     1.3 @@ -143,9 +143,11 @@
     1.4              .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
     1.5  
     1.6        val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
     1.7 -      current_DOM.removeChild(current_DOM.getLastChild())
     1.8 -      current_DOM.appendChild(node)
     1.9 -      Swing_Thread.now { setDocument(current_DOM, rcontext) }
    1.10 +      Swing_Thread.now {
    1.11 +        current_DOM.removeChild(current_DOM.getLastChild())
    1.12 +        current_DOM.appendChild(node)
    1.13 +        setDocument(current_DOM, rcontext)
    1.14 +      }
    1.15      }
    1.16  
    1.17      resize(initial_font_size)