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