# HG changeset patch
# User wenzelm
# Date 1730750101 -3600
# Node ID 30f7eb65d679c3b13a8a397bd0d868773ea813d1
# Parent  e181259e539b99c6bca1d4fa1be436a64333e3ab
clarified signature;
clarified modules;

diff -r e181259e539b -r 30f7eb65d679 etc/build.props
--- a/etc/build.props	Mon Nov 04 14:50:21 2024 +0100
+++ b/etc/build.props	Mon Nov 04 20:55:01 2024 +0100
@@ -77,6 +77,7 @@
   src/Pure/Concurrent/par_list.scala \
   src/Pure/Concurrent/synchronized.scala \
   src/Pure/GUI/color_value.scala \
+  src/Pure/GUI/font_metric.scala \
   src/Pure/GUI/desktop_app.scala \
   src/Pure/GUI/gui.scala \
   src/Pure/GUI/gui_thread.scala \
diff -r e181259e539b -r 30f7eb65d679 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -1557,10 +1557,10 @@
     import java.awt.geom.{GeneralPath, Rectangle2D}
     import java.awt.{BasicStroke, Color, Graphics2D}
 
-    val line_height = isabelle.graphview.Metrics.default.height
-    val char_width = isabelle.graphview.Metrics.default.char_width
-    val padding = isabelle.graphview.Metrics.default.space_width
-    val gap = isabelle.graphview.Metrics.default.gap
+    val line_height = Font_Metric.default.height
+    val char_width = Font_Metric.default.average_width
+    val padding = Font_Metric.default.space_width
+    val gap = Font_Metric.default.average_width * 3
 
     val graph = schedule.graph
 
@@ -1619,8 +1619,8 @@
     def paint(gfx: Graphics2D): Unit = {
       gfx.setColor(Color.LIGHT_GRAY)
       gfx.fillRect(0, 0, width, height)
-      gfx.setRenderingHints(isabelle.graphview.Metrics.rendering_hints)
-      gfx.setFont(isabelle.graphview.Metrics.default.font)
+      gfx.setRenderingHints(Font_Metric.default_hints)
+      gfx.setFont(Font_Metric.default.font)
       gfx.setStroke(new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND))
 
       draw_string(schedule.generator + ", build time: " + schedule.duration.message_hms, padding, 0)
diff -r e181259e539b -r 30f7eb65d679 src/Pure/GUI/font_metric.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/font_metric.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -0,0 +1,46 @@
+/*  Title:      Pure/GUI/gui.scala
+    Author:     Makarius
+
+Precise metric for smooth font rendering, notably for pretty-printing.
+*/
+
+package isabelle
+
+import java.util.HashMap
+import java.awt.{Font, RenderingHints}
+import java.awt.font.FontRenderContext
+import java.awt.geom.Rectangle2D
+
+
+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)
+  }
+
+  val default_font: Font = new Font("Helvetica", Font.PLAIN, 12)
+  val default_context: FontRenderContext = new FontRenderContext(null, true, true)
+  val default: Font_Metric = new Font_Metric()
+}
+
+class Font_Metric(
+  val font: Font = Font_Metric.default_font,
+  val context: FontRenderContext = Font_Metric.default_context) extends Pretty.Metric
+{
+  override def toString: String = font.toString
+
+  def string_bounds(str: String): Rectangle2D = font.getStringBounds(str, context)
+  def string_width(str: String): Double = string_bounds(str).getWidth
+
+  val space_width: Double = string_width(Symbol.space)
+  override def unit: Double = space_width max 1.0
+  override def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
+
+  protected def sample: String = "mix"
+  val height: Double = string_bounds(sample).getHeight
+  val average_width: Double = string_bounds(sample).getWidth / sample.length
+  def average: Double = average_width / unit
+}
diff -r e181259e539b -r 30f7eb65d679 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Pure/General/pretty.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -49,7 +49,7 @@
   /* text metric -- standardized to width of space */
 
   abstract class Metric {
-    val unit: Double
+    def unit: Double
     def apply(s: String): Double
   }
 
diff -r e181259e539b -r 30f7eb65d679 src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/Graphview/graphview.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -74,7 +74,7 @@
         val s =
           XML.content(Pretty.formatted(content,
             margin = options.int("graphview_content_margin").toDouble,
-            metric = metrics.Pretty_Metric))
+            metric = metrics))
         if (s.nonEmpty) s else node.toString
       }
       else node.toString
@@ -134,7 +134,7 @@
   }
 
   def paint(gfx: Graphics2D): Unit = {
-    gfx.setRenderingHints(Metrics.rendering_hints)
+    gfx.setRenderingHints(Font_Metric.default_hints)
 
     for (node <- graphview.current_node)
       Shapes.highlight_node(gfx, graphview, node)
diff -r e181259e539b -r 30f7eb65d679 src/Tools/Graphview/metrics.scala
--- a/src/Tools/Graphview/metrics.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/Graphview/metrics.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -9,53 +9,28 @@
 
 import isabelle._
 
-import java.util.HashMap
-import java.awt.{Font, RenderingHints}
-import java.awt.font.FontRenderContext
+import java.awt.Font
 import java.awt.geom.Rectangle2D
 
 
 object Metrics {
-  val rendering_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)
-  }
-
-  val font_render_context: FontRenderContext =
-    new FontRenderContext(null, true, true)
-
   def apply(font: Font): Metrics = new Metrics(font)
-
-  val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12))
+  val default: Metrics = apply(Font_Metric.default.font)
 }
 
-class Metrics private(val font: Font) {
-  def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
-  private val mix = string_bounds("mix")
-  val space_width: Double = string_bounds(" ").getWidth
-  def char_width: Double = mix.getWidth / 3
-  def height: Double = mix.getHeight
-  def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
+class Metrics private(font: Font) extends Font_Metric(font = font) {
+  val ascent: Double = font.getLineMetrics("", context).getAscent
 
-  def gap: Double = mix.getWidth.ceil
+  def gap: Double = (average_width * 3).ceil
 
-  def dummy_size2: Double = (char_width / 2).ceil
+  def dummy_size2: Double = (average_width / 2).ceil
 
   def node_width2(lines: List[String]): Double =
-    ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2)
-      .ceil
+    ((lines.foldLeft(0.0)({ case (w, s) => w max string_width(s) }) + 2 * average_width) / 2).ceil
 
   def node_height2(num_lines: Int): Double =
-    ((height.ceil * (num_lines max 1) + char_width) / 2).ceil
+    ((height.ceil * (num_lines max 1) + average_width) / 2).ceil
 
   def level_height2(num_lines: Int, num_edges: Int): Double =
     (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5))
-
-  object Pretty_Metric extends Pretty.Metric {
-    val unit: Double = space_width max 1.0
-    def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
-  }
 }
-
diff -r e181259e539b -r 30f7eb65d679 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -24,7 +24,7 @@
 
   def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit = {
     val metrics = graphview.metrics
-    val extra = metrics.char_width
+    val extra = metrics.average_width
     val info = graphview.layout.get_node(node)
 
     gfx.setColor(graphview.highlight_color)
diff -r e181259e539b -r 30f7eb65d679 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -232,13 +232,16 @@
 
   /* graphics range */
 
+  def font_metric(painter: TextAreaPainter): Font_Metric =
+    new Font_Metric(font = painter.getFont, context = painter.getFontRenderContext)
+
   case class Gfx_Range(x: Int, y: Int, length: Int)
 
   // NB: jEdit always normalizes \r\n and \r to \n
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = {
-    val metric = pretty_metric(text_area.getPainter)
-    val char_width = (metric.unit * metric.average).round.toInt
+    val metric = font_metric(text_area.getPainter)
+    val char_width = metric.average_width.round.toInt
 
     val buffer = text_area.getBuffer
 
@@ -284,23 +287,6 @@
   }
 
 
-  /* pretty text metric */
-
-  abstract class Pretty_Metric extends Pretty.Metric {
-    def average: Double
-  }
-
-  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
-    new Pretty_Metric {
-      def string_width(s: String): Double =
-        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
-
-      val unit: Double = string_width(Symbol.space) max 1.0
-      val average: Double = string_width("mix") / (3 * unit)
-      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
-    }
-
-
   /* icons */
 
   def load_icon(name: String): Icon = {
diff -r e181259e539b -r 30f7eb65d679 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -87,7 +87,7 @@
     getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
 
     if (getWidth > 0) {
-      val metric = JEdit_Lib.pretty_metric(getPainter)
+      val metric = JEdit_Lib.font_metric(getPainter)
       val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor
 
       val snapshot = current_base_snapshot
diff -r e181259e539b -r 30f7eb65d679 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -243,7 +243,7 @@
 
       val painter = pretty_text_area.getPainter
       val geometry = JEdit_Lib.window_geometry(tip, painter)
-      val metric = JEdit_Lib.pretty_metric(painter)
+      val metric = JEdit_Lib.font_metric(painter)
 
       val margin =
         ((rendering.tooltip_margin * metric.average) min