--- 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 \
--- 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)
--- /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
+}
--- 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
}
--- 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)
--- 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
- }
}
-
--- 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)
--- 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 = {
--- 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
--- 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