src/Pure/PIDE/text.scala
changeset 47542 26d0a76fef0a
parent 46712 8650d9a95736
child 48677 bd4d132e32cf
     1.1 --- a/src/Pure/PIDE/text.scala	Wed Apr 18 18:31:48 2012 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Apr 18 20:22:44 2012 +0200
     1.3 @@ -41,6 +41,8 @@
     1.4  
     1.5      override def toString = "[" + start.toString + ":" + stop.toString + "]"
     1.6  
     1.7 +    def length: Int = stop - start
     1.8 +
     1.9      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    1.10      def +(i: Offset): Range = map(_ + i)
    1.11      def -(i: Offset): Range = map(_ - i)