# HG changeset patch # User wenzelm # Date 1731237331 -3600 # Node ID 964b85e04f1f36f3decc79eaeb43b9c5b7ad2f8d # Parent 206dd586f3d7cb36914aed47e2334b9af65aa668 clarified margin operations (again, reverting 4794576828df); diff -r 206dd586f3d7 -r 964b85e04f1f src/Pure/GUI/font_metric.scala --- 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 - } } diff -r 206dd586f3d7 -r 964b85e04f1f src/Pure/GUI/rich_text.scala --- 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) } diff -r 206dd586f3d7 -r 964b85e04f1f src/Tools/jEdit/src/jedit_lib.scala --- 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) diff -r 206dd586f3d7 -r 964b85e04f1f src/Tools/jEdit/src/pretty_text_area.scala --- 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) { diff -r 206dd586f3d7 -r 964b85e04f1f src/Tools/jEdit/src/pretty_tooltip.scala --- 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)