avoid deprecated operations;

--- a/src/Tools/jEdit/src/fold_handling.scala	Wed Apr 22 18:16:27 2020 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Wed Apr 22 18:16:48 2020 +0200
@@ -11,7 +11,7 @@
 
 import javax.swing.text.Segment
 
-import scala.collection.convert.WrapAsJava
+import scala.collection.JavaConverters
 
 import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
 
@@ -43,7 +43,7 @@
         else Nil
 
       if (result.isEmpty) null
-      else WrapAsJava.seqAsJavaList(result.map(Integer.valueOf))
+      else JavaConverters.seqAsJavaList(result.map(Integer.valueOf))
     }
   }
 
@@ -78,4 +78,3 @@
     }
   }
 }
-

--- a/src/Tools/jEdit/src/keymap_merge.scala	Wed Apr 22 18:16:27 2020 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Wed Apr 22 18:16:48 2020 +0200
@@ -9,14 +9,14 @@
 
 import isabelle._
 
-import java.lang.Class
 import java.awt.{Color, Dimension, BorderLayout}
 import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
 import javax.swing.table.AbstractTableModel
 
 import scala.collection.JavaConverters
 
-import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
+import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.util.GenericGUIUtilities
 import org.jedit.keymap.{KeymapManager, Keymap}
 
 
@@ -40,7 +40,7 @@
       error("Bad shortcut property: " + quote(property))
 
     val label: String =
-      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
+      GenericGUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
 
 
     /* ignore wrt. keymap */
@@ -184,7 +184,7 @@
 
   private class Table(table_model: Table_Model) extends JPanel(new BorderLayout)
   {
-    private val cell_size = GUIUtilities.defaultTableCellSize()
+    private val cell_size = GenericGUIUtilities.defaultTableCellSize()
     private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15)
 
     val table = new JTable(table_model)

--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 22 18:16:27 2020 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 22 18:16:48 2020 +0200
@@ -234,7 +234,7 @@
       robust_body(()) {
         val x = evt.getX
         val y = evt.getY
-        val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
+        val control = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0
 
         if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {

--- a/src/Tools/jEdit/src/token_markup.scala	Wed Apr 22 18:16:27 2020 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Apr 22 18:16:48 2020 +0200
@@ -11,7 +11,7 @@
 
 import javax.swing.text.Segment
 
-import scala.collection.convert.WrapAsJava
+import scala.collection.JavaConverters
 
 import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
@@ -308,7 +308,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", WrapAsJava.seqAsJavaList(List(indent_rule))))
+          mode, "indentRules", JavaConverters.seqAsJavaList(List(indent_rule))))
     }
   }
 }