|
1 /* Title: Tools/Graphview/metrics.scala |
|
2 Author: Makarius |
|
3 |
|
4 Physical metrics for layout and painting. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.{Font, RenderingHints} |
|
13 import java.awt.font.FontRenderContext |
|
14 |
|
15 |
|
16 object Metrics |
|
17 { |
|
18 val rendering_hints: RenderingHints = |
|
19 new RenderingHints(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON) |
|
20 |
|
21 val font_render_context: FontRenderContext = |
|
22 new FontRenderContext(null, true, false) |
|
23 |
|
24 def apply(font: Font): Metrics = new Metrics(font) |
|
25 |
|
26 val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) |
|
27 } |
|
28 |
|
29 class Metrics private(val font: Font) |
|
30 { |
|
31 def string_bounds(s: String) = font.getStringBounds(s, Metrics.font_render_context) |
|
32 private val mix = string_bounds("mix") |
|
33 val space_width = string_bounds(" ").getWidth |
|
34 def char_width: Double = mix.getWidth / 3 |
|
35 def height: Double = mix.getHeight |
|
36 def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent |
|
37 def gap: Double = mix.getWidth |
|
38 def pad: Double = char_width |
|
39 |
|
40 def box_width2(node: Graph_Display.Node): Double = |
|
41 ((string_bounds(node.toString).getWidth + pad) / 2).ceil |
|
42 def box_gap: Double = gap.ceil |
|
43 def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil |
|
44 } |
|
45 |