src/Tools/jEdit/src/token_markup.scala

--- a/src/Tools/jEdit/src/token_markup.scala	Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,8 @@
 
 import isabelle._
 
+import java.util.{List => JList}
+
 import javax.swing.text.Segment
 
 import org.gjt.sp.jedit.{Mode, Buffer}
@@ -314,8 +316,7 @@
       super.loadMode(mode, xmh)
       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)))
+        Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
     }
   }
 }