--- a/src/Pure/General/file_watcher.scala Thu Jan 09 13:44:16 2020 +0100
+++ b/src/Pure/General/file_watcher.scala Thu Jan 09 13:47:08 2020 +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.JavaConversions
+import scala.collection.JavaConverters
class File_Watcher private[File_Watcher] // dummy template
@@ -102,7 +102,7 @@
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
val events =
- JavaConversions.collectionAsScalaIterable(
+ JavaConverters.collectionAsScalaIterable(
key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
val remove = if (key.reset) None else Some(dir)
val changed =
--- a/src/Pure/System/isabelle_charset.scala Thu Jan 09 13:44:16 2020 +0100
+++ b/src/Pure/System/isabelle_charset.scala Thu Jan 09 13:47:08 2020 +0100
@@ -12,6 +12,8 @@
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
import java.nio.charset.spi.CharsetProvider
+import scala.collection.JavaConverters
+
object Isabelle_Charset
{
@@ -43,10 +45,8 @@
override def charsets(): java.util.Iterator[Charset] =
{
- import scala.collection.JavaConversions._
// FIXME inactive
// Iterator(Isabelle_Charset.charset)
- Iterator()
+ JavaConverters.asJavaIterator(Iterator())
}
}
-
--- a/src/Tools/jEdit/src/keymap_merge.scala Thu Jan 09 13:44:16 2020 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala Thu Jan 09 13:47:08 2020 +0100
@@ -14,7 +14,7 @@
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
import javax.swing.table.AbstractTableModel
-import scala.collection.JavaConversions
+import scala.collection.JavaConverters
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
import org.jedit.keymap.{KeymapManager, Keymap}
@@ -68,7 +68,7 @@
if (props == null) Nil
else {
var result = List.empty[Shortcut]
- for (entry <- JavaConversions.mapAsScalaMap(props)) {
+ for (entry <- JavaConverters.mapAsScalaMap(props)) {
entry match {
case (a: String, b: String) if is_shortcut(a) =>
result ::= new Shortcut(a, b)