--- a/src/Pure/PIDE/text.scala Fri Aug 20 11:57:43 2010 +0200
+++ b/src/Pure/PIDE/text.scala Fri Aug 20 12:12:28 2010 +0200
@@ -17,6 +17,11 @@
/* range -- with total quasi-ordering */
+ object Range
+ {
+ def apply(start: Offset): Range = Range(start, start)
+ }
+
sealed case class Range(val start: Offset, val stop: Offset)
{
// denotation: {start} Un {i. start < i & i < stop}
@@ -31,9 +36,6 @@
def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
- def start_range: Range = Range(start, start)
- def stop_range: Range = Range(stop, stop)
-
def restrict(that: Range): Range =
Range(this.start max that.start, this.stop min that.stop)
}