--- a/src/Pure/GUI/font_metric.scala Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala Sun Nov 10 12:15:31 2024 +0100
@@ -25,10 +25,16 @@
class Font_Metric(
val font: Font = Font_Metric.default_font,
- val context: FontRenderContext = Font_Metric.default_context,
- standard_margin: Double => Int = _ => Pretty.default_margin.toInt) extends Pretty.Metric
+ 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
@@ -48,19 +54,4 @@
string_width(s1) / unit
}
def average: Double = average_width / unit
-
- def make_margin(margin: Int, limit: Int = -1): Int = {
- val m = (margin * average).toInt
- (if (limit < 0) m else m min limit) max 20
- }
- val margin: Int = make_margin(standard_margin(average_width))
-
- override lazy val hashCode: Int = (font, context, margin).hashCode
-
- override def equals(that: Any): Boolean =
- that match {
- case other: Font_Metric =>
- font == other.font && context == other.context && margin == other.margin
- case _ => false
- }
}