diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/PIDE/text.scala
--- 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]] =