# HG changeset patch
# User wenzelm
# Date 1517349698 -3600
# Node ID aefe7a7b330a84003c0b8350c03975c3eeba8c5e
# Parent  2b30e03a722974eb212eb851ba308e3f6f49c2fc
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;

diff -r 2b30e03a7229 -r aefe7a7b330a src/Pure/General/pretty.scala
--- 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))
 }
diff -r 2b30e03a7229 -r aefe7a7b330a src/Tools/Graphview/graphview.scala
--- 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
diff -r 2b30e03a7229 -r aefe7a7b330a src/Tools/VSCode/src/vscode_resources.scala
--- 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)
 
diff -r 2b30e03a7229 -r aefe7a7b330a src/Tools/jEdit/src/pretty_text_area.scala
--- 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 =
diff -r 2b30e03a7229 -r aefe7a7b330a src/Tools/jEdit/src/pretty_tooltip.scala
--- 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)