# HG changeset patch
# User wenzelm
# Date 1321120609 -3600
# Node ID 66395afbd915e2e84c298903437962caf5e50691
# Parent  2046f8e2ecd782a44c884b38cad691601b28c64d
tuned;

diff -r 2046f8e2ecd7 -r 66395afbd915 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 18:05:31 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 18:56:49 2011 +0100
@@ -20,6 +20,12 @@
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
+  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)
   {
     def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup)
@@ -63,18 +69,16 @@
   def + (new_markup: Text.Markup): Markup_Tree =
   {
     val new_range = new_markup.range
-    val new_info = new_markup.info
 
     branches.get(new_range) match {
-      case None =>
-        new Markup_Tree(branches, Entry(new_range, List(new_info), empty))
+      case None => new Markup_Tree(branches, Entry(new_markup, empty))
       case Some(entry) =>
         if (entry.range == new_range)
-          new Markup_Tree(branches, entry + new_info)
+          new Markup_Tree(branches, entry + new_markup.info)
         else if (entry.range.contains(new_range))
           new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
-          new Markup_Tree(Branches.empty, Entry(new_range, List(new_info), this))
+          new Markup_Tree(Branches.empty, Entry(new_markup, this))
         else {
           val body = overlapping(new_range)
           if (body.forall(e => new_range.contains(e._1))) {
@@ -83,7 +87,7 @@
                 (Branches.empty /: branches)((rest, entry) =>
                   if (body.isDefinedAt(entry._1)) rest else rest + entry)
               else branches
-            new Markup_Tree(rest, Entry(new_range, List(new_info), new Markup_Tree(body)))
+            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
           }
           else { // FIXME split markup!?
             System.err.println("Ignored overlapping markup information: " + new_markup)