output symbolic pretty printing markup and format in the front end;
authorwenzelm
Fri May 07 22:00:23 2010 +0200 (2010-05-07 ago)
changeset 3673542b7f881f5fc
parent 36734 d9b10c173330
child 36736 93753a8c9550
output symbolic pretty printing markup and format in the front end;
src/Pure/PIDE/state.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Tools/jEdit/src/jedit/html_panel.scala
     1.1 --- a/src/Pure/PIDE/state.scala	Fri May 07 20:57:37 2010 +0200
     1.2 +++ b/src/Pure/PIDE/state.scala	Fri May 07 22:00:23 2010 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4                  atts match {
     1.5                    case Position.Range(begin, end) =>
     1.6                      if (kind == Markup.ML_TYPING) {
     1.7 -                      val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
     1.8 +                      val info = Pretty.string_of(body, margin = 40)
     1.9                        state.add_markup(
    1.10                          command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
    1.11                      }
     2.1 --- a/src/Pure/System/isabelle_process.ML	Fri May 07 20:57:37 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Fri May 07 22:00:23 2010 +0200
     2.3 @@ -89,7 +89,7 @@
     2.4  
     2.5  fun init out =
     2.6   (Unsynchronized.change print_mode
     2.7 -    (fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]);
     2.8 +    (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]);
     2.9    setup_channels out |> init_message;
    2.10    OuterKeyword.report ();
    2.11    Output.status (Markup.markup Markup.ready "");
     3.1 --- a/src/Pure/System/isabelle_process.scala	Fri May 07 20:57:37 2010 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Fri May 07 22:00:23 2010 +0200
     3.3 @@ -90,7 +90,7 @@
     3.4      {
     3.5        val res =
     3.6          if (kind == Kind.STATUS) body.map(_.toString).mkString
     3.7 -        else body.map(XML.content(_).mkString).mkString
     3.8 +        else Pretty.string_of(body)
     3.9        if (props.isEmpty)
    3.10          kind.toString + " [[" + res + "]]"
    3.11        else
     4.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 07 20:57:37 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 07 22:00:23 2010 +0200
     4.3 @@ -118,9 +118,8 @@
     4.4            
     4.5          case Render(body) =>
     4.6            val doc = doc2
     4.7 -          val node =
     4.8 -            XML.document_node(doc,
     4.9 -              XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
    4.10 +          val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t)))
    4.11 +          val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
    4.12            doc.removeChild(doc.getLastChild())
    4.13            doc.appendChild(node)
    4.14            doc2 = doc1