# HG changeset patch
# User wenzelm
# Date 1521315323 -3600
# Node ID 00797fb8286945f5d2c2385ede0d8dc3a1734f57
# Parent  cd00999d2d30c166217a077849f0041003730708
clarified signature;

diff -r cd00999d2d30 -r 00797fb82869 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Mar 17 20:32:39 2018 +0100
+++ b/src/Pure/General/pretty.scala	Sat Mar 17 20:35:23 2018 +0100
@@ -40,7 +40,7 @@
     def apply(s: String): Double
   }
 
-  object Metric_Default extends Metric
+  object Default_Metric extends Metric
   {
     val unit = 1.0
     def apply(s: String): Double = s.length.toDouble
@@ -113,13 +113,13 @@
       case t :: ts => t :: force_next(ts)
     }
 
-  private val margin_default = 76.0
-  private val breakgain_default = margin_default / 20
+  val default_margin = 76.0
+  val default_breakgain = default_margin / 20
 
   def formatted(input: XML.Body,
-    margin: Double = margin_default,
-    breakgain: Double = breakgain_default,
-    metric: Metric = Metric_Default): XML.Body =
+    margin: Double = default_margin,
+    breakgain: Double = default_breakgain,
+    metric: Metric = Default_Metric): XML.Body =
   {
     val emergencypos = (margin / 2).round.toInt
 
@@ -180,8 +180,8 @@
   }
 
   def string_of(input: XML.Body,
-      margin: Double = margin_default,
-      breakgain: Double = breakgain_default,
-      metric: Metric = Metric_Default): String =
+      margin: Double = default_margin,
+      breakgain: Double = default_breakgain,
+      metric: Metric = Default_Metric): String =
     XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
 }