# HG changeset patch
# User wenzelm
# Date 1578573573 -3600
# Node ID 7f2cd237ee4ff4e453a8e51cbb4da40a92ebed2c
# Parent  ce45299cce44a7e6ea4ce83f8f3875bb7694825d
tuned -- more direct java.util.Map.of;

diff -r ce45299cce44 -r 7f2cd237ee4f src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Jan 09 08:42:01 2020 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Jan 09 13:39:33 2020 +0100
@@ -13,6 +13,8 @@
 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
   JButton, JTextField, JLabel}
 
+
+import scala.collection.JavaConverters
 import scala.swing.{ComboBox, TextArea, ScrollPane}
 import scala.swing.event.SelectionChanged
 
@@ -216,10 +218,7 @@
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
   def transform_font(font: Font, transform: AffineTransform): Font =
-  {
-    import scala.collection.JavaConversions._
-    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
-  }
+    font.deriveFont(java.util.Map.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 ce45299cce44 -r 7f2cd237ee4f src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Jan 09 08:42:01 2020 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Jan 09 13:39:33 2020 +0100
@@ -39,8 +39,8 @@
   {
     font_style(style, font0 =>
       {
-        import scala.collection.JavaConversions._
-        val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
+        val font1 =
+          font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, new java.lang.Integer(i)))
 
         def shift(y: Float): Font =
           GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))