# HG changeset patch
# User wenzelm
# Date 1578574028 -3600
# Node ID 411c0322c09d1081b082886eeaea7df61422d22d
# Parent  ec48da635e6c0f04d01e0145084bced3134dd671
eliminated deprecated scala.collection.JavaConversions;

diff -r ec48da635e6c -r 411c0322c09d src/Pure/General/file_watcher.scala
--- 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 =
diff -r ec48da635e6c -r 411c0322c09d src/Pure/System/isabelle_charset.scala
--- 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())
   }
 }
-
diff -r ec48da635e6c -r 411c0322c09d src/Tools/jEdit/src/keymap_merge.scala
--- 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)