--- a/src/Tools/jEdit/src/text_structure.scala Sun Nov 05 17:45:17 2017 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Mon Nov 06 16:03:13 2017 +0100
@@ -192,7 +192,7 @@
def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) =
{
- val text = JEdit_Lib.try_get_text(buffer, range).getOrElse("")
+ val text = JEdit_Lib.get_text(buffer, range).getOrElse("")
val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt)
val toks1 = toks.filterNot(_.is_space)
(toks1, ctxt1)