--- a/src/Pure/General/pretty.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Pure/General/pretty.scala Wed Apr 22 19:22:43 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
--- a/src/Pure/General/ssh.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Pure/General/ssh.scala Wed Apr 22 19:22:43 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)
}
--- a/src/Pure/General/timing.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Pure/General/timing.scala Wed Apr 22 19:22:43 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)
--- a/src/Pure/Thy/latex.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Pure/Thy/latex.scala Wed Apr 22 19:22:43 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)) })
--- a/src/Pure/term.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Pure/term.scala Wed Apr 22 19:22:43 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)))
--- a/src/Tools/jEdit/src/fold_handling.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Wed Apr 22 19:22:43 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 17:22:17 2020 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Apr 22 19:22:43 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 17:22:17 2020 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 22 19:22:43 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/scala_console.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Wed Apr 22 19:22:43 2020 +0200
@@ -134,7 +134,6 @@
{
override def parentClassLoader = new JARClassLoader
}
- interp.setContextClassLoader
val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
{
--- a/src/Tools/jEdit/src/token_markup.scala Wed Apr 22 17:22:17 2020 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Apr 22 19:22:43 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))))
}
}
}