clarified margin operations (again, reverting 4794576828df);

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

--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import javax.swing.JComponent
+
+
 object Rich_Text {
   def command(
     body: XML.Body = Nil,
@@ -17,4 +20,12 @@
     val markups = Command.Markups.init(Markup_Tree.from_XML(body))
     Command.unparsed(source, id = id, results = results, markups = markups)
   }
+
+  def make_margin(metric: Font_Metric, margin: Int, limit: Int = -1): Int = {
+    val m = (margin * metric.average).toInt
+    (if (limit < 0) m else m min limit) max 20
+  }
+
+  def component_margin(metric: Font_Metric, component: JComponent): Int =
+    make_margin(metric, (component.getWidth.toDouble / metric.average_width).toInt)
 }

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -235,8 +235,7 @@
   def font_metric(painter: TextAreaPainter): Font_Metric =
     new Font_Metric(
       font = painter.getFont,
-      context = painter.getFontRenderContext,
-      standard_margin = (average_width: Double) => (painter.getWidth.toDouble / average_width).toInt)
+      context = painter.getFontRenderContext)
 
   case class Gfx_Range(x: Int, y: Int, length: Int)
 

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -31,6 +31,7 @@
 object Pretty_Text_Area {
   def format_rich_texts(
     output: List[XML.Elem],
+    margin: Double,
     metric: Font_Metric,
     results: Command.Results
   ): List[Command] = {
@@ -39,7 +40,7 @@
       if (result.nonEmpty) {
         result += Rich_Text.command(body = Pretty.Separator, id = Document_ID.make())
       }
-      val body = Pretty.formatted(List(msg), margin = metric.margin, metric = metric)
+      val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
       result += Rich_Text.command(body = body, id = Markup.Serial.get(msg.markup.properties))
 
       Exn.Interrupt.expose()
@@ -108,6 +109,7 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.font_metric(getPainter)
+      val margin = Rich_Text.component_margin(metric, getPainter)
       val output = current_output
       val snapshot = current_base_snapshot
       val results = current_base_results
@@ -117,7 +119,7 @@
         Some(Future.fork {
           val (text, rendering) =
             try {
-              val rich_texts = Pretty_Text_Area.format_rich_texts(output, metric, results)
+              val rich_texts = Pretty_Text_Area.format_rich_texts(output, margin, metric, results)
               val rendering = JEdit_Rendering(snapshot, rich_texts)
               (Command.full_source(rich_texts), rendering)
             }
@@ -128,10 +130,13 @@
             }
 
           GUI_Thread.later {
-            if (metric == JEdit_Lib.font_metric(getPainter) &&
-              output == current_output &&
-              snapshot == current_base_snapshot &&
-              results == current_base_results
+            val current_metric = JEdit_Lib.font_metric(getPainter)
+            val current_margin = Rich_Text.component_margin(current_metric, getPainter)
+            if (metric == current_metric &&
+                margin == current_margin &&
+                output == current_output &&
+                snapshot == current_base_snapshot &&
+                results == current_base_results
             ) {
               current_rendering = rendering
               JEdit_Lib.buffer_edit(getBuffer) {

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 10 11:55:36 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 10 12:15:31 2024 +0100
@@ -248,7 +248,7 @@
       val geometry = JEdit_Lib.window_geometry(pretty_tooltip, painter)
       val metric = JEdit_Lib.font_metric(painter)
       val margin =
-        metric.make_margin(rendering.tooltip_margin,
+        Rich_Text.make_margin(metric, rendering.tooltip_margin,
           limit = ((w_max - geometry.deco_width) / metric.average_width).toInt)
 
       val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)