src/Pure/PIDE/markup_tree.scala
changeset 44379 1079ab6b342b
parent 43714 3749d1e6dde9
child 45455 4f974c0c5c2f
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 14:15:52 2011 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 16:12:23 2011 +0200
     1.3 @@ -22,10 +22,7 @@
     1.4      type Entry = (Text.Info[Any], Markup_Tree)
     1.5      type T = SortedMap[Text.Range, Entry]
     1.6  
     1.7 -    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
     1.8 -      {
     1.9 -        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    1.10 -      })
    1.11 +    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
    1.12  
    1.13      def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
    1.14      def single(entry: Entry): T = update(empty, entry)