--- a/src/Tools/jEdit/src/document_model.scala Sun Nov 05 17:45:17 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 06 16:03:13 2017 +0100
@@ -406,7 +406,7 @@
{
/* text */
- def try_get_text(range: Text.Range): Option[String] =
+ def get_text(range: Text.Range): Option[String] =
range.try_substring(content.text)
@@ -473,8 +473,8 @@
{
/* text */
- def try_get_text(range: Text.Range): Option[String] =
- JEdit_Lib.try_get_text(buffer, range)
+ def get_text(range: Text.Range): Option[String] =
+ JEdit_Lib.get_text(buffer, range)
/* header */