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