# HG changeset patch
# User wenzelm
# Date 1259964611 -3600
# Node ID b316d05a66a4c75f28acbb9bc2f077d81dfbb17d
# Parent  94ef0ff39c211cde63d30b9d3cc3f932e4d91001
tuned message markup;

diff -r 94ef0ff39c21 -r b316d05a66a4 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Fri Dec 04 23:07:40 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Fri Dec 04 23:10:11 2009 +0100
@@ -62,6 +62,13 @@
 <style media="all" type="text/css">
 """ +
   try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+"""
+body {
+  white-space: pre;
+  font-family: IsabelleMono;
+  font-size: 14pt;
+}
+""" +
   try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
 """
 </style>
@@ -70,7 +77,7 @@
 """)))
   }
 
-  val empty_body = XML.document_node(doc, XML.Elem("body", Nil, List(XML.Text("empty"))))
+  val empty_body = XML.document_node(doc, HTML.body(Nil))
   doc.appendChild(empty_body)
 
   panel.setDocument(doc, rcontext)
@@ -83,8 +90,8 @@
 
     val node =
       if (cmd == null) empty_body
-      else XML.document_node(doc, XML.Elem("body", Nil, List(XML.Text(XML.content(
-                cmd.results(theory_view.current_document)).mkString))))
+      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])