1/* Title: Tools/Graphview/metrics.scala 2 Author: Makarius 3 4Physical metrics for layout and painting. 5*/ 6 7package isabelle.graphview 8 9 10import isabelle._ 11 12import java.awt.{Font, RenderingHints} 13import java.awt.font.FontRenderContext 14import java.awt.geom.Rectangle2D 15 16 17object Metrics 18{ 19 val rendering_hints: RenderingHints = 20 { 21 val hints = new java.util.HashMap[RenderingHints.Key, AnyRef] 22 hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON) 23 hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON) 24 new RenderingHints(hints) 25 } 26 27 val font_render_context: FontRenderContext = 28 new FontRenderContext(null, true, true) 29 30 def apply(font: Font): Metrics = new Metrics(font) 31 32 val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) 33} 34 35class Metrics private(val font: Font) 36{ 37 def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context) 38 private val mix = string_bounds("mix") 39 val space_width: Double = 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 44 def gap: Double = mix.getWidth.ceil 45 46 def dummy_size2: Double = (char_width / 2).ceil 47 48 def node_width2(lines: List[String]): Double = 49 (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil 50 51 def node_height2(num_lines: Int): Double = 52 ((height.ceil * (num_lines max 1) + char_width) / 2).ceil 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: Double = space_width max 1.0 60 def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit 61 } 62} 63 64