--- a/src/Pure/General/pretty.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/pretty.scala Thu Mar 04 15:41:46 2021 +0100
@@ -75,7 +75,7 @@
{
val (line, rest) =
Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
- val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+ val len1 = (line.foldLeft(0.0) { case (l, t) => l + t.length }) max len
(rest: @unchecked) match {
case Break(true, _, ind) :: rest1 =>
body_length(Break(false, indent1 + ind, 0) :: rest1, len1)