--- 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
+ }
}