src/Tools/jEdit/src/pretty_tooltip.scala

         XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
           (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
-        if (h <= h_max)
-          (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
+        if (h <= h_max) {
+          split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+        }
         else margin
       val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
 
       new Dimension(w min w_max, h min h_max)
     }