make double-sure that line context is present, e.g. relevant for last line after visible text;
authorwenzelm
Sat, 18 Oct 2014 21:26:01 +0200
changeset 58701 cc83453fac15
parent 58700 4717d18cc619
child 58702 39866de9d988
make double-sure that line context is present, e.g. relevant for last line after visible text;
src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 20:56:16 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 21:26:01 2014 +0200
@@ -15,8 +15,8 @@
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.jedit.{jEdit, Mode}
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet,
-  ModeProvider, XModeHandler, SyntaxStyle}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
+  ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
 import org.gjt.sp.jedit.textarea.{TextArea, Selection}
 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
 
@@ -193,9 +193,14 @@
   def buffer_line_context(buffer: JEditBuffer, line: Int): Option[Line_Context] =
     Untyped.get(buffer, "lineMgr") match {
       case line_mgr: LineManager =>
-        line_mgr.getLineContext(line) match {
-          case c: Line_Context => Some(c)
-          case _ => None
+        def context =
+          line_mgr.getLineContext(line) match {
+            case c: Line_Context => Some(c)
+            case _ => None
+          }
+        context orElse {
+          buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+          context
         }
       case _ => None
     }