diff -r 2b9ffffccc9b -r cfb165af55c5 src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:00:31 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:05:05 2024 +0100
@@ -6,7 +6,6 @@
 
 package isabelle
 
-import java.util.HashMap
 import java.awt.{Font, RenderingHints}
 import java.awt.font.FontRenderContext
 import java.awt.geom.Rectangle2D
@@ -14,12 +13,10 @@
 
 object Font_Metric {
   val default_hints: RenderingHints =
-  {
-    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)
-  }
+    new RenderingHints(
+      java.util.Map.of(
+        RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON,
+        RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON))
 
   val default_font: Font = new Font("Helvetica", Font.PLAIN, 12)
   val default_context: FontRenderContext = new FontRenderContext(null, true, true)