src/Pure/PIDE/markup_tree.scala

 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 
-object Markup_Tree
-{
+object Markup_Tree {
   /* construct trees */
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
   def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =

     }
 
 
   /* tree building blocks */
 
-  object Entry
-  {
+  object Entry {
     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
       Entry(markup.range, List(markup.info), subtree)
   }
 
   sealed case class Entry(
     range: Text.Range,
     rev_markup: List[XML.Elem],
-    subtree: Markup_Tree)
-  {
+    subtree: Markup_Tree
+  ) {
     def markup: List[XML.Elem] = rev_markup.reverse
 
-    def filter_markup(elements: Markup.Elements): List[XML.Elem] =
-    {
+    def filter_markup(elements: Markup.Elements): List[XML.Elem] = {
       var result: List[XML.Elem] = Nil
       for (elem <- rev_markup if elements(elem.name))
         result ::= elem
       result
     }
 
     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
     def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
   }
 
-  object Branches
-  {
+  object Branches {
     type T = SortedMap[Text.Range, Entry]
     val empty: T = SortedMap.empty(Text.Range.Ordering)
   }
 
 

       case List(XML.Elem(markup1, body1)) =>
         strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
       case _ => (elems, body)
     }
 
-  private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
-    {
-      val (offset, markup_trees) = acc
-
-      strip_elems(Nil, List(tree)) match {
-        case (Nil, body) =>
-          (offset + XML.text_length(body), markup_trees)
-
-        case (elems, body) =>
-          val (end_offset, subtrees) =
-             body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
-          if (offset == end_offset) acc
-          else {
-            val range = Text.Range(offset, end_offset)
-            val entry = Entry(range, elems, merge_disjoint(subtrees))
-            (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
-          }
-      }
-    }
+  private def make_trees(
+    acc: (Int, List[Markup_Tree]),
+    tree: XML.Tree
+  ): (Int, List[Markup_Tree]) = {
+    val (offset, markup_trees) = acc
+
+    strip_elems(Nil, List(tree)) match {
+      case (Nil, body) =>
+        (offset + XML.text_length(body), markup_trees)
+
+      case (elems, body) =>
+        val (end_offset, subtrees) =
+           body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
+        if (offset == end_offset) acc
+        else {
+          val range = Text.Range(offset, end_offset)
+          val entry = Entry(range, elems, merge_disjoint(subtrees))
+          (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
+        }
+    }
+  }
 
   def from_XML(body: XML.Body): Markup_Tree =
     merge_disjoint(body.foldLeft((0, List.empty[Markup_Tree]))(make_trees)._2)
 }
 
 
-final class Markup_Tree private(val branches: Markup_Tree.Branches.T)
-{
+final class Markup_Tree private(val branches: Markup_Tree.Branches.T) {
   import Markup_Tree._
 
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 

   def restrict(range: Text.Range): Markup_Tree =
     new Markup_Tree(overlapping(range))
 
   def is_empty: Boolean = branches.isEmpty
 
-  def + (new_markup: Text.Markup): Markup_Tree =
-  {
+  def + (new_markup: Text.Markup): Markup_Tree = {
     val new_range = new_markup.range
 
     branches.get(new_range) match {
       case None => new Markup_Tree(branches, Entry(new_markup, empty))
       case Some(entry) =>

           }
         }
     }
   }
 
-  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
-  {
+  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree = {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
       tree2.branches.foldLeft(tree1) {
         case (tree, (range, entry)) =>
           if (!range.overlaps(root_range)) tree
           else {

       if (tree1.is_empty) tree2
       else merge_trees(tree1, tree2)
     }
   }
 
-  def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
-    result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
-  {
-    def results(x: A, entry: Entry): Option[A] =
-    {
+  def cumulate[A](
+    root_range: Text.Range,
+    root_info: A,
+    elements: Markup.Elements,
+    result: (A, Text.Markup) => Option[A]
+  ): List[Text.Info[A]] = {
+    def results(x: A, entry: Entry): Option[A] = {
       var y = x
       var changed = false
       for {
         elem <- entry.filter_markup(elements)
         y1 <- result(y, Text.Info(entry.range, elem))

       if (changed) Some(y) else None
     }
 
     def traverse(
       last: Text.Offset,
-      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
-    {
+      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]
+    ): List[Text.Info[A]] = {
       stack match {
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
           val subtree = entry.subtree.overlapping(subrange).toList
           val start = subrange.start

     }
     traverse(root_range.start,
       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
 
-  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
-  {
+  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body = {
     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
       if (start == stop) Nil
       else List(XML.Text(text.subSequence(start, stop).toString))
 
     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =

           if (!elements(elem.name)) b
           else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
           else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
       }
 
-    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
-      : XML.Body =
-    {
+    def make_body(
+      elem_range: Text.Range,
+      elem_markup: List[XML.Elem],
+      entries: Branches.T
+    ) : XML.Body = {
       val body = new mutable.ListBuffer[XML.Tree]
       var last = elem_range.start
       for ((range, entry) <- entries) {
         val subrange = range.restrict(elem_range)
         body ++= make_text(last, subrange.start)