# HG changeset patch # User wenzelm # Date 1625084067 -7200 # Node ID 1d0d9772fff06983bf727ea3295a662cf5762153 # Parent 506734c805ac4133f762417aa799dafa78f903ac tuned imports; diff -r 506734c805ac -r 1d0d9772fff0 src/Pure/GUI/gui.scala --- 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) diff -r 506734c805ac -r 1d0d9772fff0 src/Pure/General/file_watcher.scala --- 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]) { diff -r 506734c805ac -r 1d0d9772fff0 src/Pure/General/ssh.scala --- 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 diff -r 506734c805ac -r 1d0d9772fff0 src/Pure/System/isabelle_charset.scala --- 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() } } diff -r 506734c805ac -r 1d0d9772fff0 src/Pure/Tools/spell_checker.scala --- 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) } diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/Graphview/metrics.scala --- 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) diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src-base/pide_docking_framework.scala --- 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 diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src/fold_handling.scala --- 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 = diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src/keymap_merge.scala --- 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 = diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src/syntax_style.scala --- 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)) diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src/text_structure.scala --- 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) => diff -r 506734c805ac -r 1d0d9772fff0 src/Tools/jEdit/src/token_markup.scala --- 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))) } } }