src/Tools/jEdit/src/token_markup.scala

--- 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))
       }
     }