src/Pure/PIDE/line.scala
changeset 67014 e6a695d6a6b2
parent 66923 914935f8a462
child 70792 ea2834adf8de
--- a/src/Pure/PIDE/line.scala	Sun Nov 05 17:45:17 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Mon Nov 06 16:03:13 2017 +0100
@@ -128,7 +128,7 @@
 
     lazy val text: String = Document.text(lines)
 
-    def try_get_text(range: Text.Range): Option[String] =
+    def get_text(range: Text.Range): Option[String] =
       if (text_range.contains(range)) Some(range.substring(text)) else None
 
     override def toString: String = text