src/Tools/jEdit/src/text_structure.scala
changeset 67014 e6a695d6a6b2
parent 66183 c67933ea9234
child 68730 0bc491938780
--- 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)