src/Tools/Graphview/metrics.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 59389 c427f3de9050
permissions -rw-r--r--
more strict AFP properties;
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@59384
    14
import java.awt.geom.Rectangle2D
wenzelm@59290
    15
wenzelm@59290
    16
wenzelm@59290
    17
object Metrics
wenzelm@59290
    18
{
wenzelm@59290
    19
  val rendering_hints: RenderingHints =
wenzelm@59389
    20
  {
wenzelm@59389
    21
    val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
wenzelm@59389
    22
    hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
wenzelm@59389
    23
    hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
wenzelm@59389
    24
    new RenderingHints(hints)
wenzelm@59389
    25
  }
wenzelm@59290
    26
wenzelm@59290
    27
  val font_render_context: FontRenderContext =
wenzelm@59389
    28
    new FontRenderContext(null, true, true)
wenzelm@59290
    29
wenzelm@59290
    30
  def apply(font: Font): Metrics = new Metrics(font)
wenzelm@59290
    31
wenzelm@59290
    32
  val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12))
wenzelm@59290
    33
}
wenzelm@59290
    34
wenzelm@59290
    35
class Metrics private(val font: Font)
wenzelm@59290
    36
{
wenzelm@59384
    37
  def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
wenzelm@59290
    38
  private val mix = string_bounds("mix")
wenzelm@59290
    39
  val space_width = string_bounds(" ").getWidth
wenzelm@59290
    40
  def char_width: Double = mix.getWidth / 3
wenzelm@59290
    41
  def height: Double = mix.getHeight
wenzelm@59290
    42
  def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
wenzelm@59290
    43
wenzelm@59384
    44
  def gap: Double = mix.getWidth.ceil
wenzelm@59302
    45
wenzelm@59388
    46
  def dummy_size2: Double = (char_width / 2).ceil
wenzelm@59384
    47
wenzelm@59384
    48
  def node_width2(lines: List[String]): Double =
wenzelm@59388
    49
    (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
wenzelm@59302
    50
wenzelm@59384
    51
  def node_height2(num_lines: Int): Double =
wenzelm@59388
    52
    ((height.ceil * (num_lines max 1) + char_width) / 2).ceil
wenzelm@59384
    53
wenzelm@59384
    54
  def level_height2(num_lines: Int, num_edges: Int): Double =
wenzelm@59384
    55
    (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5))
wenzelm@59384
    56
wenzelm@59384
    57
  object Pretty_Metric extends Pretty.Metric
wenzelm@59384
    58
  {
wenzelm@59384
    59
    val unit = space_width max 1.0
wenzelm@59384
    60
    def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
wenzelm@59384
    61
  }
wenzelm@59290
    62
}
wenzelm@59290
    63