src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Wed Apr 18 18:31:48 2012 +0200
+++ b/src/Pure/PIDE/text.scala	Wed Apr 18 20:22:44 2012 +0200
@@ -41,6 +41,8 @@
 
     override def toString = "[" + start.toString + ":" + stop.toString + "]"
 
+    def length: Int = stop - start
+
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
     def -(i: Offset): Range = map(_ - i)