# HG changeset patch # User wenzelm # Date 1614802776 -3600 # Node ID 279e45248e9d54577f72d834fdaacdb61f2f2d29 # Parent 54b43bcf1df3f7dab7c9f90f03dfd72701c6c40a tuned --- fewer warnings; diff -r 54b43bcf1df3 -r 279e45248e9d src/Pure/General/file_watcher.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) { diff -r 54b43bcf1df3 -r 279e45248e9d src/Tools/jEdit/src/fold_handling.scala --- 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 } } diff -r 54b43bcf1df3 -r 279e45248e9d src/Tools/jEdit/src/keymap_merge.scala --- 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) 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))) } } }