tuned --- fewer warnings;
authorwenzelm
Wed, 03 Mar 2021 21:19:36 +0100
changeset 73353 279e45248e9d
parent 73352 54b43bcf1df3
child 73354 79b120d1c1a3
tuned --- fewer warnings;
src/Pure/General/file_watcher.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/keymap_merge.scala
src/Tools/jEdit/src/token_markup.scala
--- 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)))
     }
   }
 }