src/Pure/PIDE/markup_tree.scala
changeset 46712 8650d9a95736
parent 46178 1c5c88f6feb5
child 47539 436ae5ea4f80
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 16:56:25 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 17:13:25 2012 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Markup_Tree private(branches: Markup_Tree.Branches.T)
     1.8 +final class Markup_Tree private(branches: Markup_Tree.Branches.T)
     1.9  {
    1.10    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
    1.11      this(branches + (entry.range -> entry))