make double-sure that line context is present, e.g. relevant for last line after visible text;
--- 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
}