src/Pure/PIDE/markup_tree.scala
changeset 43714 3749d1e6dde9
parent 43520 cec9b95fa35d
child 44379 1079ab6b342b
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Jul 08 22:00:53 2011 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 09 12:56:51 2011 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -case class Markup_Tree(val branches: Markup_Tree.Branches.T)
     1.8 +sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
     1.9  {
    1.10    import Markup_Tree._
    1.11