src/Tools/Graphview/metrics.scala
changeset 59302 4d985afc0565
parent 59293 305e79989d48
child 59384 c75327a34960
     1.1 --- a/src/Tools/Graphview/metrics.scala	Tue Jan 06 11:58:57 2015 +0100
     1.2 +++ b/src/Tools/Graphview/metrics.scala	Tue Jan 06 16:33:30 2015 +0100
     1.3 @@ -38,8 +38,16 @@
     1.4    def pad_x: Double = char_width * 1.5
     1.5    def pad_y: Double = char_width
     1.6  
     1.7 +  def dummy_width2: Double = (pad_x / 2).ceil
     1.8 +
     1.9    def box_width2(node: Graph_Display.Node): Double =
    1.10      ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
    1.11 +
    1.12 +  def box_width2(vertex: Layout.Vertex): Double =
    1.13 +    vertex match {
    1.14 +      case Layout.Node(node) => box_width2(node)
    1.15 +      case _: Layout.Dummy => dummy_width2
    1.16 +    }
    1.17    def box_gap: Double = gap.ceil
    1.18    def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
    1.19  }