src/Tools/jEdit/src/token_markup.scala
changeset 73882 01efb7cbf365
parent 73618 4b413b78cd94
child 73909 1d0d9772fff0
equal deleted inserted replaced
73881:b1272ec71568 73882:01efb7cbf365
   310     for (mode <- orig_provider.getModes) addMode(mode)
   310     for (mode <- orig_provider.getModes) addMode(mode)
   311 
   311 
   312     override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
   312     override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
   313     {
   313     {
   314       super.loadMode(mode, xmh)
   314       super.loadMode(mode, xmh)
   315       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
   315       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
   316       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
   316       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
   317         Untyped.set[java.util.List[IndentRule]](
   317         Untyped.set[java.util.List[IndentRule]](
   318           mode, "indentRules", java.util.List.of(indent_rule)))
   318           mode, "indentRules", java.util.List.of(indent_rule)))
   319     }
   319     }
   320   }
   320   }