clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
--- 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))
}
--- a/src/Tools/Graphview/graphview.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/Graphview/graphview.scala Tue Jan 30 23:01:38 2018 +0100
@@ -75,8 +75,9 @@
def node_text(node: Graph_Display.Node, content: XML.Body): String =
if (show_content) {
val s =
- XML.content(Pretty.formatted(
- content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric))
+ XML.content(Pretty.formatted(content,
+ margin = options.int("graphview_content_margin").toDouble,
+ metric = metrics.Pretty_Metric))
if (s.nonEmpty) s else node.toString
}
else node.toString
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 30 23:01:38 2018 +0100
@@ -347,7 +347,7 @@
output_text(XML.content(xml))
def output_pretty(body: XML.Body, margin: Int): String =
- output_text(Pretty.string_of(body, margin))
+ output_text(Pretty.string_of(body, margin = margin))
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Jan 30 23:01:38 2018 +0100
@@ -129,7 +129,7 @@
val base_snapshot = current_base_snapshot
val base_results = current_base_results
- val formatted_body = Pretty.formatted(current_body, margin, metric)
+ val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
future_refresh.map(_.cancel)
future_refresh =
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Jan 30 23:01:38 2018 +0100
@@ -259,7 +259,7 @@
((rendering.tooltip_margin * metric.average) min
((w_max - geometry.deco_width) / metric.unit).toInt) max 20
- val formatted = Pretty.formatted(info.info, margin, metric)
+ val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
val lines =
XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)