diff -r 65a247444100 -r 31e9920a0dc1 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Jan 11 20:01:55 2017 +0100
@@ -104,6 +104,10 @@
     }
     lazy val text: String = lines.mkString("", "\n", "")
 
+    def try_get_text(range: Text.Range): Option[String] =
+      if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
+      else None
+
     override def toString: String = text
 
     override def equals(that: Any): Boolean =