# HG changeset patch
# User wenzelm
# Date 1260140721 -3600
# Node ID e377d3d6910a92e48b5a44bc120448ff3cd60bc0
# Parent  a2ed621f5f52339d4e7926b8466d9592e0d08f26
use IsabelleText font;
explicit <pre> element;
relayout in swing thread -- paranoia mode;

diff -r a2ed621f5f52 -r e377d3d6910a src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Sun Dec 06 20:50:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Dec 07 00:05:21 2009 +0100
@@ -72,8 +72,7 @@
   try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
 """
 body {
-  white-space: pre;
-  font-family: IsabelleMono;
+  font-family: IsabelleText;
   font-size: 14pt;
 }
 """ +
@@ -85,7 +84,7 @@
 """)))
   }
 
-  val empty_body = XML.document_node(doc, HTML.body(Nil))
+  val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
   doc.appendChild(empty_body)
 
   panel.setDocument(doc, rcontext)
@@ -98,10 +97,16 @@
 
     val node =
       if (cmd == null) empty_body
-      else XML.document_node(doc, HTML.body(
-        cmd.results(theory_view.current_document).map((t: XML.Tree) => HTML.div(HTML.spans(t)))))
-    doc.removeChild(doc.getLastChild())
-    doc.appendChild(node)
-    panel.delayedRelayout(node.asInstanceOf[NodeImpl])
+      else {
+        val xml = XML.elem(HTML.BODY,
+          cmd.results(theory_view.current_document).
+            map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
+        XML.document_node(doc, xml)
+      }
+    Swing_Thread.later {
+      doc.removeChild(doc.getLastChild())
+      doc.appendChild(node)
+      panel.delayedRelayout(node.asInstanceOf[NodeImpl])
+    }
   })
 }