author | wenzelm |
Wed, 30 Jun 2021 22:14:27 +0200 | |
changeset 73909 | 1d0d9772fff0 |
parent 73359 | d8a0e996614b |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
59290 | 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 |
||
73909 | 12 |
import java.util.HashMap |
59290 | 13 |
import java.awt.{Font, RenderingHints} |
14 |
import java.awt.font.FontRenderContext |
|
59384 | 15 |
import java.awt.geom.Rectangle2D |
59290 | 16 |
|
17 |
||
18 |
object Metrics |
|
19 |
{ |
|
20 |
val rendering_hints: RenderingHints = |
|
59389
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
21 |
{ |
73909 | 22 |
val hints = new HashMap[RenderingHints.Key, AnyRef] |
59389
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
23 |
hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON) |
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
24 |
hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON) |
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
25 |
new RenderingHints(hints) |
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
26 |
} |
59290 | 27 |
|
28 |
val font_render_context: FontRenderContext = |
|
59389
c427f3de9050
prefer fractional font metrics, for proper scaling of node size;
wenzelm
parents:
59388
diff
changeset
|
29 |
new FontRenderContext(null, true, true) |
59290 | 30 |
|
31 |
def apply(font: Font): Metrics = new Metrics(font) |
|
32 |
||
33 |
val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) |
|
34 |
} |
|
35 |
||
36 |
class Metrics private(val font: Font) |
|
37 |
{ |
|
59384 | 38 |
def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context) |
59290 | 39 |
private val mix = string_bounds("mix") |
71383 | 40 |
val space_width: Double = string_bounds(" ").getWidth |
59290 | 41 |
def char_width: Double = mix.getWidth / 3 |
42 |
def height: Double = mix.getHeight |
|
43 |
def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent |
|
44 |
||
59384 | 45 |
def gap: Double = mix.getWidth.ceil |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59293
diff
changeset
|
46 |
|
59388 | 47 |
def dummy_size2: Double = (char_width / 2).ceil |
59384 | 48 |
|
49 |
def node_width2(lines: List[String]): Double = |
|
73359 | 50 |
((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2) |
51 |
.ceil |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59293
diff
changeset
|
52 |
|
59384 | 53 |
def node_height2(num_lines: Int): Double = |
59388 | 54 |
((height.ceil * (num_lines max 1) + char_width) / 2).ceil |
59384 | 55 |
|
56 |
def level_height2(num_lines: Int, num_edges: Int): Double = |
|
57 |
(node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5)) |
|
58 |
||
59 |
object Pretty_Metric extends Pretty.Metric |
|
60 |
{ |
|
71383 | 61 |
val unit: Double = space_width max 1.0 |
59384 | 62 |
def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit |
63 |
} |
|
59290 | 64 |
} |
65 |