# HG changeset patch
# User wenzelm
# Date 1624715536 -7200
# Node ID 01efb7cbf365f9722fb79e7a52155cfc3c9fbb19
# Parent  b1272ec715680e0a4cd7d3c3e4ed795344edb139
tuned;

diff -r b1272ec71568 -r 01efb7cbf365 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 26 15:33:27 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 26 15:52:16 2021 +0200
@@ -312,7 +312,7 @@
     override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
     {
       super.loadMode(mode, xmh)
-      Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
+      Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[java.util.List[IndentRule]](
           mode, "indentRules", java.util.List.of(indent_rule)))