src/Pure/PIDE/text.scala
changeset 58749 83b0f633190e
parent 57912 dd9550f84106
child 60215 5fb4990dfc73
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Oct 21 15:21:44 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Oct 21 17:49:51 2014 +0200
     1.3 @@ -51,6 +51,8 @@
     1.4      def is_singularity: Boolean = start == stop
     1.5      def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
     1.6  
     1.7 +    def touches(i: Offset): Boolean = start <= i && i <= stop
     1.8 +
     1.9      def contains(i: Offset): Boolean = start == i || start < i && i < stop
    1.10      def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    1.11      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)