src/Tools/Graphview/metrics.scala
author wenzelm
Tue Jan 06 16:33:30 2015 +0100 (2015-01-06)
changeset 59302 4d985afc0565
parent 59293 305e79989d48
child 59384 c75327a34960
permissions -rw-r--r--
explict layout graph structure, with dummies and coordinates;
explicit metrics for dummy box;
tuned signature;
misc tuning;
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@59293
    38
  def pad_x: Double = char_width * 1.5
wenzelm@59293
    39
  def pad_y: Double = char_width
wenzelm@59290
    40
wenzelm@59302
    41
  def dummy_width2: Double = (pad_x / 2).ceil
wenzelm@59302
    42
wenzelm@59290
    43
  def box_width2(node: Graph_Display.Node): Double =
wenzelm@59293
    44
    ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
wenzelm@59302
    45
wenzelm@59302
    46
  def box_width2(vertex: Layout.Vertex): Double =
wenzelm@59302
    47
    vertex match {
wenzelm@59302
    48
      case Layout.Node(node) => box_width2(node)
wenzelm@59302
    49
      case _: Layout.Dummy => dummy_width2
wenzelm@59302
    50
    }
wenzelm@59290
    51
  def box_gap: Double = gap.ceil
wenzelm@59290
    52
  def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
wenzelm@59290
    53
}
wenzelm@59290
    54