src/Pure/PIDE/text.scala
changeset 38662 4d4553e09337
parent 38578 1ebc6b76e5ff
child 38725 3d9d5ff80f6f
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Aug 24 21:34:38 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Aug 24 23:49:07 2010 +0200
     1.3 @@ -32,6 +32,9 @@
     1.4      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     1.5      def +(i: Offset): Range = map(_ + i)
     1.6      def -(i: Offset): Range = map(_ - i)
     1.7 +
     1.8 +    def is_singleton: Boolean = start == stop
     1.9 +
    1.10      def contains(i: Offset): Boolean = start == i || start < i && i < stop
    1.11      def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    1.12      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)