diff -r 20304512a33b -r c137a9f038a6 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -73,6 +73,10 @@
       else Some(Range(this.start min that.start, this.stop max that.stop))
 
     def substring(text: String): String = text.substring(start, stop)
+
+    def try_substring(text: String): Option[String] =
+      try { Some(substring(text)) }
+      catch { case _: IndexOutOfBoundsException => None }
   }