--- 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)