--- a/src/Pure/PIDE/text.scala Fri May 01 15:33:43 2015 +0200
+++ b/src/Pure/PIDE/text.scala Sun May 03 00:01:10 2015 +0200
@@ -34,7 +34,7 @@
}
}
- sealed case class Range(val start: Offset, val stop: Offset)
+ sealed case class Range(start: Offset, stop: Offset)
{
// denotation: {start} Un {i. start < i & i < stop}
if (start > stop)
@@ -124,7 +124,7 @@
/* information associated with text range */
- sealed case class Info[A](val range: Text.Range, val info: A)
+ sealed case class Info[A](range: Text.Range, info: A)
{
def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))