src/Tools/Graphview/metrics.scala
author wenzelm
Mon Jan 05 21:47:12 2015 +0100 (2015-01-05)
changeset 59290 569a8109eeb2
child 59293 305e79989d48
permissions -rw-r--r--
separate module Metrics;
maintain static metrics (with font) and visible_graph via layout;
wenzelm@59290
     1
/*  Title:      Tools/Graphview/metrics.scala
wenzelm@59290
     2
    Author:     Makarius
wenzelm@59290
     3
wenzelm@59290
     4
Physical metrics for layout and painting.
wenzelm@59290
     5
*/
wenzelm@59290
     6
wenzelm@59290
     7
package isabelle.graphview
wenzelm@59290
     8
wenzelm@59290
     9
wenzelm@59290
    10
import isabelle._
wenzelm@59290
    11
wenzelm@59290
    12
import java.awt.{Font, RenderingHints}
wenzelm@59290
    13
import java.awt.font.FontRenderContext
wenzelm@59290
    14
wenzelm@59290
    15
wenzelm@59290
    16
object Metrics
wenzelm@59290
    17
{
wenzelm@59290
    18
  val rendering_hints: RenderingHints =
wenzelm@59290
    19
    new RenderingHints(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
wenzelm@59290
    20
wenzelm@59290
    21
  val font_render_context: FontRenderContext =
wenzelm@59290
    22
    new FontRenderContext(null, true, false)
wenzelm@59290
    23
wenzelm@59290
    24
  def apply(font: Font): Metrics = new Metrics(font)
wenzelm@59290
    25
wenzelm@59290
    26
  val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12))
wenzelm@59290
    27
}
wenzelm@59290
    28
wenzelm@59290
    29
class Metrics private(val font: Font)
wenzelm@59290
    30
{
wenzelm@59290
    31
  def string_bounds(s: String) = font.getStringBounds(s, Metrics.font_render_context)
wenzelm@59290
    32
  private val mix = string_bounds("mix")
wenzelm@59290
    33
  val space_width = string_bounds(" ").getWidth
wenzelm@59290
    34
  def char_width: Double = mix.getWidth / 3
wenzelm@59290
    35
  def height: Double = mix.getHeight
wenzelm@59290
    36
  def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
wenzelm@59290
    37
  def gap: Double = mix.getWidth
wenzelm@59290
    38
  def pad: Double = char_width
wenzelm@59290
    39
wenzelm@59290
    40
  def box_width2(node: Graph_Display.Node): Double =
wenzelm@59290
    41
    ((string_bounds(node.toString).getWidth + pad) / 2).ceil
wenzelm@59290
    42
  def box_gap: Double = gap.ceil
wenzelm@59290
    43
  def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
wenzelm@59290
    44
}
wenzelm@59290
    45