--- a/src/Pure/General/pretty.scala Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/pretty.scala Fri Mar 27 22:01:27 2020 +0100
@@ -6,6 +6,8 @@
package isabelle
+import scala.annotation.tailrec
+
object Pretty
{
@@ -69,7 +71,7 @@
{
val indent1 = force_nat(indent)
- def body_length(prts: List[Tree], len: Double): Double =
+ @tailrec def body_length(prts: List[Tree], len: Double): Double =
{
val (line, rest) =
Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
@@ -104,7 +106,7 @@
private def force_break(tree: Tree): Tree =
tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
- private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
+ private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break)
private def force_next(trees: List[Tree]): List[Tree] =
trees match {
@@ -113,8 +115,8 @@
case t :: ts => t :: force_next(ts)
}
- val default_margin = 76.0
- val default_breakgain = default_margin / 20
+ val default_margin: Double = 76.0
+ val default_breakgain: Double = default_margin / 20
def formatted(input: XML.Body,
margin: Double = default_margin,