src/Pure/PIDE/text.scala
changeset 56172 31289387fdf8
parent 48677 bd4d132e32cf
child 56308 ebd3bf053969
--- a/src/Pure/PIDE/text.scala	Mon Mar 17 11:33:09 2014 +0100
+++ b/src/Pure/PIDE/text.scala	Mon Mar 17 11:39:46 2014 +0100
@@ -26,6 +26,8 @@
   {
     def apply(start: Offset): Range = Range(start, start)
 
+    val offside: Range = apply(-1)
+
     object Ordering extends scala.math.Ordering[Text.Range]
     {
       def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2