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