src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 05 17:45:17 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 06 16:03:13 2017 +0100
@@ -171,7 +171,7 @@
 
   /* get text */
 
-  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
+  def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
@@ -262,7 +262,7 @@
       try {
         val p = text_area.offsetToXY(range.start)
         val (q, r) =
-          if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
+          if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
             (text_area.offsetToXY(stop - 1), char_width)
           else if (stop >= end)
             (text_area.offsetToXY(end), char_width * (stop - end))