# HG changeset patch
# User wenzelm
# Date 1413660361 -7200
# Node ID cc83453fac1504d2764bfc8db7080e81c3563f17
# Parent  4717d18cc6191c2f399bd0ae84fe4b2beecc6651
make double-sure that line context is present, e.g. relevant for last line after visible text;

diff -r 4717d18cc619 -r cc83453fac15 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
     }