# HG changeset patch
# User wenzelm
# Date 1273262423 -7200
# Node ID 42b7f881f5fc12d4f161c2afca899c0f4873381c
# Parent  d9b10c1733303b3499a789a961621eb243ff2606
output symbolic pretty printing markup and format in the front end;

diff -r d9b10c173330 -r 42b7f881f5fc src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Fri May 07 20:57:37 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Fri May 07 22:00:23 2010 +0200
@@ -84,7 +84,7 @@
                 atts match {
                   case Position.Range(begin, end) =>
                     if (kind == Markup.ML_TYPING) {
-                      val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
+                      val info = Pretty.string_of(body, margin = 40)
                       state.add_markup(
                         command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
                     }
diff -r d9b10c173330 -r 42b7f881f5fc src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri May 07 20:57:37 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri May 07 22:00:23 2010 +0200
@@ -89,7 +89,7 @@
 
 fun init out =
  (Unsynchronized.change print_mode
-    (fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]);
+    (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]);
   setup_channels out |> init_message;
   OuterKeyword.report ();
   Output.status (Markup.markup Markup.ready "");
diff -r d9b10c173330 -r 42b7f881f5fc src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri May 07 20:57:37 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri May 07 22:00:23 2010 +0200
@@ -90,7 +90,7 @@
     {
       val res =
         if (kind == Kind.STATUS) body.map(_.toString).mkString
-        else body.map(XML.content(_).mkString).mkString
+        else Pretty.string_of(body)
       if (props.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
diff -r d9b10c173330 -r 42b7f881f5fc src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 07 20:57:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 07 22:00:23 2010 +0200
@@ -118,9 +118,8 @@
           
         case Render(body) =>
           val doc = doc2
-          val node =
-            XML.document_node(doc,
-              XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
+          val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t)))
+          val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
           doc.removeChild(doc.getLastChild())
           doc.appendChild(node)
           doc2 = doc1