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