equal
deleted
inserted
replaced
44 def gap: Double = mix.getWidth.ceil |
44 def gap: Double = mix.getWidth.ceil |
45 |
45 |
46 def dummy_size2: Double = (char_width / 2).ceil |
46 def dummy_size2: Double = (char_width / 2).ceil |
47 |
47 |
48 def node_width2(lines: List[String]): Double = |
48 def node_width2(lines: List[String]): Double = |
49 (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil |
49 ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2) |
|
50 .ceil |
50 |
51 |
51 def node_height2(num_lines: Int): Double = |
52 def node_height2(num_lines: Int): Double = |
52 ((height.ceil * (num_lines max 1) + char_width) / 2).ceil |
53 ((height.ceil * (num_lines max 1) + char_width) / 2).ceil |
53 |
54 |
54 def level_height2(num_lines: Int, num_edges: Int): Double = |
55 def level_height2(num_lines: Int, num_edges: Int): Double = |