--- a/src/Tools/Graphview/metrics.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/Graphview/metrics.scala Thu Mar 04 15:41:46 2021 +0100
@@ -46,7 +46,8 @@
def dummy_size2: Double = (char_width / 2).ceil
def node_width2(lines: List[String]): Double =
- (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
+ ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2)
+ .ceil
def node_height2(num_lines: Int): Double =
((height.ceil * (num_lines max 1) + char_width) / 2).ceil