# HG changeset patch
# User wenzelm
# Date 1730753674 -3600
# Node ID 33e39b9bc4613b42597b7068a74eea5b2bed3124
# Parent  1b9ea66810ffca2de86e93f1de424b01b835155b
support value-oriented Font_Metric, e.g. for caching Pretty output;

diff -r 1b9ea66810ff -r 33e39b9bc461 src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:25:26 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:54:34 2024 +0100
@@ -28,6 +28,13 @@
   val context: FontRenderContext = Font_Metric.default_context) extends Pretty.Metric
 {
   override def toString: String = font.toString
+  override def hashCode: Int = font.hashCode
+
+  override def equals(that: Any): Boolean =
+    that match {
+      case other: Font_Metric => font == other.font && context == other.context
+      case _ => false
+    }
 
   def string_bounds(str: String): Rectangle2D = font.getStringBounds(str, context)
   def string_width(str: String): Double = string_bounds(str).getWidth