# HG changeset patch
# User wenzelm
# Date 1347972672 -7200
# Node ID 1053a564dd251e9bbee4d7d66de1108b2ec7a9ef
# Parent  8b402b550a80e4f14ad8952de247e72c2f722ae6
some actual rich text markup via XML.content_markup;
tuned signature;

diff -r 8b402b550a80 -r 1053a564dd25 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -146,7 +146,7 @@
 
   def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    XML.content(formatted(input, margin, metric)).mkString
+    XML.content(formatted(input, margin, metric))
 
 
   /* unformatted output */
@@ -164,5 +164,5 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString
+  def str_of(input: XML.Body): String = XML.content(unformatted(input))
 }
diff -r 8b402b550a80 -r 1053a564dd25 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -109,8 +109,7 @@
 
   def rich_text(id: Document.Command_ID, body: XML.Body): Command =
   {
-    val text = XML.content(body).mkString
-    val markup = Markup_Tree.empty  // FIXME
+    val (text, markup) = XML.content_markup(body)
     unparsed(id, text, markup)
   }
 
diff -r 8b402b550a80 -r 1053a564dd25 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -12,8 +12,6 @@
 import java.lang.ref.WeakReference
 import javax.xml.parsers.DocumentBuilderFactory
 
-import scala.collection.mutable
-
 
 object XML
 {
@@ -71,18 +69,33 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* text content */
+  /* content -- text and markup */
+
+  private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
+  {
+    var text = new StringBuilder
+    var markup_tree = Markup_Tree.empty
 
-  def content_stream(tree: Tree): Stream[String] =
-    tree match {
-      case Elem(_, body) => content_stream(body)
-      case Text(content) => Stream(content)
-    }
-  def content_stream(body: Body): Stream[String] =
-    body.toStream.flatten(content_stream(_))
+    def traverse(tree: Tree): Unit =
+      tree match {
+        case Elem(markup, trees) =>
+          val offset = text.length
+          trees.foreach(traverse)
+          val end_offset = text.length
+          // FIXME proper order!?
+          if (record_markup)
+            markup_tree +=
+              isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
+        case Text(s) => text.append(s)
+      }
 
-  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
-  def content(body: Body): Iterator[String] = content_stream(body).iterator
+    body.foreach(traverse)
+    (text.toString, markup_tree)
+  }
+
+  def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)
+  def content(body: Body): String = make_content(body, false)._1
+  def content(tree: Tree): String = make_content(List(tree), false)._1
 
 
 
diff -r 8b402b550a80 -r 1053a564dd25 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -125,7 +125,7 @@
   /* global state */
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
-  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
+  def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   private def phase_=(new_phase: Session.Phase)
@@ -311,7 +311,7 @@
           }
 
         case Isabelle_Markup.Assign_Execs if output.is_protocol =>
-          XML.content(output.body).mkString match {
+          XML.content(output.body) match {
             case Protocol.Assign(id, assign) =>
               try {
                 val cmds = global_state >>> (_.assign(id, assign))
@@ -328,7 +328,7 @@
           }
 
         case Isabelle_Markup.Removed_Versions if output.is_protocol =>
-          XML.content(output.body).mkString match {
+          XML.content(output.body) match {
             case Protocol.Removed(removed) =>
               try {
                 global_state >> (_.removed_versions(removed))
@@ -339,7 +339,7 @@
 
         case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
           Future.fork {
-            val arg = XML.content(output.body).mkString
+            val arg = XML.content(output.body)
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
diff -r 8b402b550a80 -r 1053a564dd25 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -20,7 +20,7 @@
 
 object Pretty_Text_Area
 {
-  def document_state(formatted_body: XML.Body): Document.State =
+  def document_state(formatted_body: XML.Body): (String, Document.State) =
   {
     val command = Command.rich_text(Document.new_id(), formatted_body)
     val node_name = command.node_name
@@ -39,7 +39,7 @@
         .define_version(version1, state0.the_assignment(version0))
         .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
 
-    state1
+    (command.source, state1)
   }
 }
 
@@ -52,19 +52,22 @@
   private var current_font_size: Int = 12
   private var current_margin: Int = 0
   private var current_body: XML.Body = Nil
-  private var current_rendering: Isabelle_Rendering = make_rendering()
+  private var current_rendering: Isabelle_Rendering = text_rendering()._2
 
-  private def make_rendering(): Isabelle_Rendering =
+  val text_area = new JEditEmbeddedTextArea
+  val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
+
+  private def text_rendering(): (String, Isabelle_Rendering) =
   {
     Swing_Thread.require()
 
     val body =
       Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
-    Isabelle_Rendering(Pretty_Text_Area.document_state(body).snapshot(), Isabelle.options.value)
-  }
+    val (text, state) = Pretty_Text_Area.document_state(body)
+    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
 
-  val text_area = new JEditEmbeddedTextArea
-  val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
+    (text, rendering)
+  }
 
   def refresh()
   {
@@ -80,8 +83,8 @@
     current_font_metrics = painter.getFontMetrics(font)
     current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
 
-    val text =
-      Pretty.string_of(current_body, current_margin, Pretty.font_metric(current_font_metrics))
+    val (text, rendering) = text_rendering()
+    current_rendering = rendering
 
     val buffer = text_area.getBuffer
     try {
diff -r 8b402b550a80 -r 1053a564dd25 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -31,7 +31,7 @@
       react {
         case output: Isabelle_Process.Output =>
           if (output.is_stdout || output.is_stderr)
-            Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
+            Swing_Thread.later { text_area.append(XML.content(output.message)) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }