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