--- a/src/Tools/jEdit/src/token_markup.scala Sun May 02 20:51:21 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Sun May 02 21:46:59 2021 +0200
@@ -30,6 +30,9 @@
def init(mode: String): Line_Context =
new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
+ def refresh(buffer: JEditBuffer, line: Int): Unit =
+ buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+
def before(buffer: JEditBuffer, line: Int): Line_Context =
if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
else after(buffer, line - 1)
@@ -42,8 +45,9 @@
case c: Line_Context => Some(c)
case _ => None
}
+
context getOrElse {
- buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+ refresh(buffer, line)
context getOrElse init(JEdit_Lib.buffer_mode(buffer))
}
}