diff -r 54b43bcf1df3 -r 279e45248e9d src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Mar 03 20:56:30 2021 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Mar 03 21:19:36 2021 +0100
@@ -11,8 +11,6 @@
 
 import javax.swing.text.Segment
 
-import scala.collection.JavaConverters
-
 import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler}
@@ -308,7 +306,7 @@
       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", JavaConverters.seqAsJavaList(List(indent_rule))))
+          mode, "indentRules", java.util.List.of(indent_rule)))
     }
   }
 }