# HG changeset patch
# User wenzelm
# Date 1321021522 -3600
# Node ID 9ba615ac75fb77450acaf9c5f1eb03f9ecca1918
# Parent  4f974c0c5c2fb0b9bcd29c287f5d56c52ccfe265
more abstract Markup_Tree;

diff -r 4f974c0c5c2f -r 9ba615ac75fb src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:24:38 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 15:25:22 2011 +0100
@@ -15,14 +15,16 @@
 
 object Markup_Tree
 {
-  /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
+  type Select[A] = PartialFunction[Text.Markup, A]
+
+  val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
   object Branches
   {
     type Entry = (Text.Markup, Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
-    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
+    val empty: T = SortedMap.empty(Text.Range.Ordering)
 
     def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
     def single(entry: Entry): T = update(empty, entry)
@@ -38,14 +40,10 @@
       }
     }
   }
-
-  val empty = new Markup_Tree(Branches.empty)
-
-  type Select[A] = PartialFunction[Text.Markup, A]
 }
 
 
-sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+class Markup_Tree private(branches: Markup_Tree.Branches.T)
 {
   import Markup_Tree._