src/Pure/PIDE/text.scala
changeset 43714 3749d1e6dde9
parent 43650 f00da558b78e
child 44379 1079ab6b342b
     1.1 --- a/src/Pure/PIDE/text.scala	Fri Jul 08 22:00:53 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Jul 09 12:56:51 2011 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5    /* information associated with text range */
     1.6  
     1.7 -  case class Info[A](val range: Text.Range, val info: A)
     1.8 +  sealed case class Info[A](val range: Text.Range, val info: A)
     1.9    {
    1.10      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.11      def try_restrict(r: Text.Range): Option[Info[A]] =