src/Pure/PIDE/text.scala
changeset 56590 d01d183e84ea
parent 56473 5b5c750e9763
child 56746 d37a5d09a277
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 15 13:07:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 15 16:44:06 2014 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4      def -(i: Offset): Range = if (i == 0) this else map(_ - i)
     1.5  
     1.6      def is_singularity: Boolean = start == stop
     1.7 +    def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
     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