# HG changeset patch # User wenzelm # Date 1282686547 -7200 # Node ID 4d4553e0933777c6308e3aa9aded4d7827766f60 # Parent f1ba2ae8e58a58988dd14c4c72f202d085b0765b Text.Range.is_singleton; diff -r f1ba2ae8e58a -r 4d4553e09337 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Tue Aug 24 21:34:38 2010 +0200 +++ b/src/Pure/PIDE/text.scala Tue Aug 24 23:49:07 2010 +0200 @@ -32,6 +32,9 @@ def map(f: Offset => Offset): Range = Range(f(start), f(stop)) def +(i: Offset): Range = map(_ + i) def -(i: Offset): Range = map(_ - i) + + def is_singleton: Boolean = start == stop + def contains(i: Offset): Boolean = start == i || start < i && i < stop def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)