# HG changeset patch
# User wenzelm
# Date 1587573501 -7200
# Node ID 97975476547c99374aedffd6b678561255e3f715
# Parent  ad91684444d717a457b5c06c9679d742d98ddc07# Parent  39613d6e20218b35038c2c05da737f4626035bab
merged

diff -r ad91684444d7 -r 97975476547c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Pure/General/pretty.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -76,7 +76,7 @@
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
       val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
-      rest match {
+      (rest: @unchecked) match {
         case Break(true, _, ind) :: rest1 =>
           body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
         case Nil => len1
diff -r ad91684444d7 -r 97975476547c src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Pure/General/ssh.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -13,7 +13,8 @@
 import scala.util.matching.Regex
 
 import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
-  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
+  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS,
+  JSchException}
 
 
 object SSH
@@ -78,8 +79,13 @@
 
     val identity_files =
       space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
-    for (identity_file <- identity_files if identity_file.is_file)
-      jsch.addIdentity(File.platform_path(identity_file))
+    for (identity_file <- identity_files if identity_file.is_file) {
+      try { jsch.addIdentity(File.platform_path(identity_file)) }
+      catch {
+        case exn: JSchException =>
+          error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
+      }
+    }
 
     new Context(options, jsch)
   }
diff -r ad91684444d7 -r 97975476547c src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Pure/General/timing.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -60,7 +60,7 @@
   {
     val factor_text =
       factor match {
-        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
+        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
         case None => ""
       }
     if (resources.seconds >= 3.0)
diff -r ad91684444d7 -r 97975476547c src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Pure/Thy/latex.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -147,7 +147,8 @@
 
     def error_suffix1(lines: List[String]): Option[String] =
     {
-      val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
+      val lines1 =
+        lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
diff -r ad91684444d7 -r 97975476547c src/Pure/term.scala
--- a/src/Pure/term.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Pure/term.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -195,7 +195,7 @@
         lookup(x) match {
           case Some(y) => y
           case None =>
-            x match {
+            (x: @unchecked) match {
               case PBound(_) => store(x)
               case Abst(name, typ, body) =>
                 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
diff -r ad91684444d7 -r 97975476547c src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Wed Apr 22 18:38:21 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 @@
     }
   }
 }
-
diff -r ad91684444d7 -r 97975476547c src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Wed Apr 22 18:38:21 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)
diff -r ad91684444d7 -r 97975476547c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 22 18:38:21 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) {
diff -r ad91684444d7 -r 97975476547c src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Wed Apr 22 18:38:21 2020 +0200
@@ -134,7 +134,6 @@
     {
       override def parentClassLoader = new JARClassLoader
     }
-    interp.setContextClassLoader
 
     val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
     {
diff -r ad91684444d7 -r 97975476547c src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Apr 22 18:38:21 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))))
     }
   }
 }