--- a/src/Pure/General/file_watcher.scala Wed Mar 03 20:56:30 2021 +0100
+++ b/src/Pure/General/file_watcher.scala Wed Mar 03 21:19:36 2021 +0100
@@ -12,7 +12,7 @@
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY}
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
class File_Watcher private[File_Watcher] // dummy template
@@ -101,9 +101,8 @@
val (remove, changed) =
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
- val events =
- JavaConverters.collectionAsScalaIterable(
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
+ val events: Iterable[WatchEvent[JPath]] =
+ key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
val remove = if (key.reset) None else Some(dir)
val changed =
(Set.empty[JFile] /: events.iterator) {
--- a/src/Tools/jEdit/src/fold_handling.scala Wed Mar 03 20:56:30 2021 +0100
+++ b/src/Tools/jEdit/src/fold_handling.scala Wed Mar 03 21:19:36 2021 +0100
@@ -11,7 +11,7 @@
import javax.swing.text.Segment
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
@@ -42,8 +42,7 @@
takeWhile(_.improper).map(_ => structure.depth max 0).toList
else Nil
- if (result.isEmpty) null
- else JavaConverters.seqAsJavaList(result.map(Integer.valueOf))
+ if (result.isEmpty) null else result.map(Integer.valueOf).asJava
}
}
--- a/src/Tools/jEdit/src/keymap_merge.scala Wed Mar 03 20:56:30 2021 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Mar 03 21:19:36 2021 +0100
@@ -13,7 +13,7 @@
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
import javax.swing.table.AbstractTableModel
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
import org.gjt.sp.jedit.{jEdit, View}
import org.gjt.sp.util.GenericGUIUtilities
@@ -68,7 +68,7 @@
if (props == null) Nil
else {
var result = List.empty[Shortcut]
- for (entry <- JavaConverters.mapAsScalaMap(props)) {
+ for (entry <- props.asScala) {
entry match {
case (a: String, b: String) if is_shortcut(a) =>
result ::= new Shortcut(a, b)
--- 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)))
}
}
}