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