src/Tools/Graphview/metrics.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 59389 c427f3de9050
permissions -rw-r--r--
tuned imports;
     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 import java.awt.geom.Rectangle2D
    15 
    16 
    17 object 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 
    35 class 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 = 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 = 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