equal
deleted
inserted
replaced
36 def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent |
36 def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent |
37 def gap: Double = mix.getWidth |
37 def gap: Double = mix.getWidth |
38 def pad_x: Double = char_width * 1.5 |
38 def pad_x: Double = char_width * 1.5 |
39 def pad_y: Double = char_width |
39 def pad_y: Double = char_width |
40 |
40 |
|
41 def dummy_width2: Double = (pad_x / 2).ceil |
|
42 |
41 def box_width2(node: Graph_Display.Node): Double = |
43 def box_width2(node: Graph_Display.Node): Double = |
42 ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil |
44 ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil |
|
45 |
|
46 def box_width2(vertex: Layout.Vertex): Double = |
|
47 vertex match { |
|
48 case Layout.Node(node) => box_width2(node) |
|
49 case _: Layout.Dummy => dummy_width2 |
|
50 } |
43 def box_gap: Double = gap.ceil |
51 def box_gap: Double = gap.ceil |
44 def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil |
52 def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil |
45 } |
53 } |
46 |
54 |