# HG changeset patch
# User wenzelm
# Date 1348132193 -7200
# Node ID 99ed1f422635a6d8f9693e8354cf03cfae0a2888
# Parent  76ecbc7f36832be6a7ec0e0b32107579208a1dbc
tuned signature;

diff -r 76ecbc7f3683 -r 99ed1f422635 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Sep 20 10:43:04 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Sep 20 11:09:53 2012 +0200
@@ -112,7 +112,8 @@
 
   def rich_text(id: Document.Command_ID, body: XML.Body): Command =
   {
-    val (text, markup) = XML.content_markup(body)
+    val text = XML.content(body)
+    val markup = Markup_Tree.from_XML(body)
     unparsed(id, text, markup)
   }
 
diff -r 76ecbc7f3683 -r 99ed1f422635 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 10:43:04 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 11:09:53 2012 +0200
@@ -48,6 +48,28 @@
     def reverse_markup(branches: T): T =
       (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
   }
+
+
+  /* XML representation */
+
+  def from_XML(body: XML.Body): Markup_Tree =
+  {
+    var offset = 0
+    var markup_tree = empty
+
+    def traverse(tree: XML.Tree): Unit =
+      tree match {
+        case XML.Elem(markup, trees) =>
+          val start = offset
+          trees.foreach(traverse)
+          val stop = offset
+          markup_tree += Text.Info(Text.Range(start, stop), XML.Elem(markup, Nil))
+        case XML.Text(s) => offset += s.length
+      }
+    body.foreach(traverse)
+
+    markup_tree.reverse_markup
+  }
 }
 
 
diff -r 76ecbc7f3683 -r 99ed1f422635 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Sep 20 10:43:04 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Sep 20 11:09:53 2012 +0200
@@ -69,32 +69,31 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* content -- text and markup */
-
-  private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
-  {
-    val text = new StringBuilder
-    var markup_tree = Markup_Tree.empty
+  /* traverse text */
 
-    def traverse(tree: Tree): Unit =
-      tree match {
-        case Elem(markup, trees) =>
-          val offset = text.length
-          trees.foreach(traverse)
-          val end_offset = text.length
-          if (record_markup)
-            markup_tree +=
-              isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
-        case Text(s) => text.append(s)
+  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
+  {
+    def traverse(x: A, t: Tree): A =
+      t match {
+        case Elem(_, ts) => (x /: ts)(traverse)
+        case Text(s) => op(x, s)
       }
-
-    body.foreach(traverse)
-    (text.toString, markup_tree.reverse_markup)
+    (a /: body)(traverse)
   }
 
-  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
+  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
+
+
+  /* text content */
+
+  def content(body: Body): String =
+  {
+    val text = new StringBuilder(text_length(body))
+    traverse_text(body)(()) { case (_, s) => text.append(s) }
+    text.toString
+  }
+
+  def content(tree: Tree): String = content(List(tree))