--- a/src/Pure/General/pretty.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Pure/General/pretty.scala Tue Jan 30 23:01:38 2018 +0100
@@ -114,11 +114,13 @@
}
private val margin_default = 76.0
+ private val breakgain_default = margin_default / 20
- def formatted(input: XML.Body, margin: Double = margin_default,
+ def formatted(input: XML.Body,
+ margin: Double = margin_default,
+ breakgain: Double = breakgain_default,
metric: Metric = Metric_Default): XML.Body =
{
- val breakgain = margin / 20
val emergencypos = (margin / 2).round.toInt
def make_tree(inp: XML.Body): List[Tree] =
@@ -177,7 +179,9 @@
format(make_tree(input), 0, 0.0, Text()).content
}
- def string_of(input: XML.Body, margin: Double = margin_default,
+ def string_of(input: XML.Body,
+ margin: Double = margin_default,
+ breakgain: Double = breakgain_default,
metric: Metric = Metric_Default): String =
- XML.content(formatted(input, margin, metric))
+ XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
}