src/Pure/PIDE/xml.scala
changeset 49416 1053a564dd25
parent 46839 f7232c078fa5
child 49417 c5a8592fb5d3
     1.1 --- a/src/Pure/PIDE/xml.scala	Tue Sep 18 13:36:28 2012 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Tue Sep 18 14:51:12 2012 +0200
     1.3 @@ -12,8 +12,6 @@
     1.4  import java.lang.ref.WeakReference
     1.5  import javax.xml.parsers.DocumentBuilderFactory
     1.6  
     1.7 -import scala.collection.mutable
     1.8 -
     1.9  
    1.10  object XML
    1.11  {
    1.12 @@ -71,18 +69,33 @@
    1.13    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    1.14  
    1.15  
    1.16 -  /* text content */
    1.17 +  /* content -- text and markup */
    1.18 +
    1.19 +  private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
    1.20 +  {
    1.21 +    var text = new StringBuilder
    1.22 +    var markup_tree = Markup_Tree.empty
    1.23  
    1.24 -  def content_stream(tree: Tree): Stream[String] =
    1.25 -    tree match {
    1.26 -      case Elem(_, body) => content_stream(body)
    1.27 -      case Text(content) => Stream(content)
    1.28 -    }
    1.29 -  def content_stream(body: Body): Stream[String] =
    1.30 -    body.toStream.flatten(content_stream(_))
    1.31 +    def traverse(tree: Tree): Unit =
    1.32 +      tree match {
    1.33 +        case Elem(markup, trees) =>
    1.34 +          val offset = text.length
    1.35 +          trees.foreach(traverse)
    1.36 +          val end_offset = text.length
    1.37 +          // FIXME proper order!?
    1.38 +          if (record_markup)
    1.39 +            markup_tree +=
    1.40 +              isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
    1.41 +        case Text(s) => text.append(s)
    1.42 +      }
    1.43  
    1.44 -  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
    1.45 -  def content(body: Body): Iterator[String] = content_stream(body).iterator
    1.46 +    body.foreach(traverse)
    1.47 +    (text.toString, markup_tree)
    1.48 +  }
    1.49 +
    1.50 +  def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)
    1.51 +  def content(body: Body): String = make_content(body, false)._1
    1.52 +  def content(tree: Tree): String = make_content(List(tree), false)._1
    1.53  
    1.54  
    1.55