--- a/src/Pure/GUI/gui.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/GUI/gui.scala Wed Jun 30 22:14:27 2021 +0200
@@ -6,6 +6,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
@@ -299,7 +300,7 @@
font.getLineMetrics("", new FontRenderContext(null, false, false))
def transform_font(font: Font, transform: AffineTransform): Font =
- font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
+ font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
--- a/src/Pure/General/file_watcher.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/General/file_watcher.scala Wed Jun 30 22:14:27 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.io.{File => JFile}
import java.nio.file.FileSystems
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
@@ -102,7 +103,7 @@
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
val events: Iterable[WatchEvent[JPath]] =
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
+ key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala
val remove = if (key.reset) None else Some(dir)
val changed =
events.iterator.foldLeft(Set.empty[JFile]) {
--- a/src/Pure/General/ssh.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/General/ssh.scala Wed Jun 30 22:14:27 2021 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.util.{Map => JMap, HashMap}
+import java.util.{Map => JMap}
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
import scala.collection.mutable
--- a/src/Pure/System/isabelle_charset.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/System/isabelle_charset.scala Wed Jun 30 22:14:27 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.nio.Buffer
import java.nio.{ByteBuffer, CharBuffer}
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
@@ -45,6 +46,6 @@
{
// FIXME inactive
// Iterator(Isabelle_Charset.charset)
- java.util.List.of[Charset]().listIterator()
+ JList.of[Charset]().listIterator()
}
}
--- a/src/Pure/Tools/spell_checker.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/Tools/spell_checker.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
import java.lang.Class
+import java.util.{List => JList}
import scala.collection.mutable
import scala.annotation.tailrec
@@ -223,7 +224,7 @@
{
val res =
Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
- invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+ invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString)
if (res.isEmpty) None else Some(res)
}
--- a/src/Tools/Graphview/metrics.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/Graphview/metrics.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.HashMap
import java.awt.{Font, RenderingHints}
import java.awt.font.FontRenderContext
import java.awt.geom.Rectangle2D
@@ -18,7 +19,7 @@
{
val rendering_hints: RenderingHints =
{
- val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
+ val hints = new HashMap[RenderingHints.Key, AnyRef]
hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
new RenderingHints(hints)
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{List => JList}
import java.awt.event.{ActionListener, ActionEvent}
import javax.swing.{JPopupMenu, JMenuItem}
@@ -42,7 +43,7 @@
}
case panel: PanelWindowContainer =>
- val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
+ val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
val wins =
(for {
entry <- entries.iterator
--- a/src/Tools/jEdit/src/fold_handling.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import scala.jdk.CollectionConverters._
@@ -32,7 +34,7 @@
Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
override def getPrecedingFoldLevels(
- buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
+ buffer: JEditBuffer, line: Int, seg: Segment, level: Int): JList[Integer] =
{
val structure = Token_Markup.Line_Context.after(buffer, line).structure
val result =
--- a/src/Tools/jEdit/src/keymap_merge.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Properties => JProperties}
import java.awt.{Color, Dimension, BorderLayout}
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
import javax.swing.table.AbstractTableModel
@@ -64,7 +65,7 @@
/* content wrt. keymap */
- def convert_properties(props: java.util.Properties): List[Shortcut] =
+ def convert_properties(props: JProperties): List[Shortcut] =
if (props == null) Nil
else {
var result = List.empty[Shortcut]
@@ -82,7 +83,7 @@
{
val keymap_shortcuts =
if (keymap == null) Nil
- else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
+ else convert_properties(Untyped.get[JProperties](keymap, "props"))
for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
val conflicts =
--- a/src/Tools/jEdit/src/syntax_style.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Map => JMap}
import java.awt.{Font, Color}
import java.awt.font.TextAttribute
import java.awt.geom.AffineTransform
@@ -40,8 +41,7 @@
{
font_style(style, font0 =>
{
- val font1 =
- font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
+ val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
def shift(y: Float): Font =
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
--- a/src/Tools/jEdit/src/text_structure.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -45,7 +47,7 @@
private val keyword_close = Keyword.proof_close
def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
- actions: java.util.List[IndentAction]): Unit =
+ actions: JList[IndentAction]): Unit =
{
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
--- a/src/Tools/jEdit/src/token_markup.scala Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import org.gjt.sp.jedit.{Mode, Buffer}
@@ -314,8 +316,7 @@
super.loadMode(mode, xmh)
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", java.util.List.of(indent_rule)))
+ Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
}
}
}