tuned signature;
authorwenzelm
Thu Sep 20 11:09:53 2012 +0200 (2012-09-20 ago)
changeset 4946699ed1f422635
parent 49465 76ecbc7f3683
child 49467 25b7e843e124
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Sep 20 10:43:04 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Sep 20 11:09:53 2012 +0200
     1.3 @@ -112,7 +112,8 @@
     1.4  
     1.5    def rich_text(id: Document.Command_ID, body: XML.Body): Command =
     1.6    {
     1.7 -    val (text, markup) = XML.content_markup(body)
     1.8 +    val text = XML.content(body)
     1.9 +    val markup = Markup_Tree.from_XML(body)
    1.10      unparsed(id, text, markup)
    1.11    }
    1.12  
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 10:43:04 2012 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 11:09:53 2012 +0200
     2.3 @@ -48,6 +48,28 @@
     2.4      def reverse_markup(branches: T): T =
     2.5        (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
     2.6    }
     2.7 +
     2.8 +
     2.9 +  /* XML representation */
    2.10 +
    2.11 +  def from_XML(body: XML.Body): Markup_Tree =
    2.12 +  {
    2.13 +    var offset = 0
    2.14 +    var markup_tree = empty
    2.15 +
    2.16 +    def traverse(tree: XML.Tree): Unit =
    2.17 +      tree match {
    2.18 +        case XML.Elem(markup, trees) =>
    2.19 +          val start = offset
    2.20 +          trees.foreach(traverse)
    2.21 +          val stop = offset
    2.22 +          markup_tree += Text.Info(Text.Range(start, stop), XML.Elem(markup, Nil))
    2.23 +        case XML.Text(s) => offset += s.length
    2.24 +      }
    2.25 +    body.foreach(traverse)
    2.26 +
    2.27 +    markup_tree.reverse_markup
    2.28 +  }
    2.29  }
    2.30  
    2.31  
     3.1 --- a/src/Pure/PIDE/xml.scala	Thu Sep 20 10:43:04 2012 +0200
     3.2 +++ b/src/Pure/PIDE/xml.scala	Thu Sep 20 11:09:53 2012 +0200
     3.3 @@ -69,32 +69,31 @@
     3.4    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
     3.5  
     3.6  
     3.7 -  /* content -- text and markup */
     3.8 -
     3.9 -  private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
    3.10 -  {
    3.11 -    val text = new StringBuilder
    3.12 -    var markup_tree = Markup_Tree.empty
    3.13 +  /* traverse text */
    3.14  
    3.15 -    def traverse(tree: Tree): Unit =
    3.16 -      tree match {
    3.17 -        case Elem(markup, trees) =>
    3.18 -          val offset = text.length
    3.19 -          trees.foreach(traverse)
    3.20 -          val end_offset = text.length
    3.21 -          if (record_markup)
    3.22 -            markup_tree +=
    3.23 -              isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
    3.24 -        case Text(s) => text.append(s)
    3.25 +  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    3.26 +  {
    3.27 +    def traverse(x: A, t: Tree): A =
    3.28 +      t match {
    3.29 +        case Elem(_, ts) => (x /: ts)(traverse)
    3.30 +        case Text(s) => op(x, s)
    3.31        }
    3.32 -
    3.33 -    body.foreach(traverse)
    3.34 -    (text.toString, markup_tree.reverse_markup)
    3.35 +    (a /: body)(traverse)
    3.36    }
    3.37  
    3.38 -  def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)
    3.39 -  def content(body: Body): String = make_content(body, false)._1
    3.40 -  def content(tree: Tree): String = make_content(List(tree), false)._1
    3.41 +  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    3.42 +
    3.43 +
    3.44 +  /* text content */
    3.45 +
    3.46 +  def content(body: Body): String =
    3.47 +  {
    3.48 +    val text = new StringBuilder(text_length(body))
    3.49 +    traverse_text(body)(()) { case (_, s) => text.append(s) }
    3.50 +    text.toString
    3.51 +  }
    3.52 +
    3.53 +  def content(tree: Tree): String = content(List(tree))
    3.54  
    3.55  
    3.56