src/Pure/PIDE/line.scala

--- a/src/Pure/PIDE/line.scala	Wed Dec 28 11:28:31 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 16:45:00 2016 +0100
@@ -123,6 +123,11 @@
       move(offset, 0, lines)
     }
 
+    def range(text_range: Text.Range, length: Length = Length): Range =
+      Range(
+        position(text_range.start, length),
+        position(text_range.stop, length))
+
     def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
     {
       val l = pos.line