clarified signature;
authorwenzelm
Sat Mar 17 20:35:23 2018 +0100 (14 months ago)
changeset 6789600797fb82869
parent 67895 cd00999d2d30
child 67897 a5b9d1f51b04
clarified signature;
src/Pure/General/pretty.scala
     1.1 --- a/src/Pure/General/pretty.scala	Sat Mar 17 20:32:39 2018 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Sat Mar 17 20:35:23 2018 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4      def apply(s: String): Double
     1.5    }
     1.6  
     1.7 -  object Metric_Default extends Metric
     1.8 +  object Default_Metric extends Metric
     1.9    {
    1.10      val unit = 1.0
    1.11      def apply(s: String): Double = s.length.toDouble
    1.12 @@ -113,13 +113,13 @@
    1.13        case t :: ts => t :: force_next(ts)
    1.14      }
    1.15  
    1.16 -  private val margin_default = 76.0
    1.17 -  private val breakgain_default = margin_default / 20
    1.18 +  val default_margin = 76.0
    1.19 +  val default_breakgain = default_margin / 20
    1.20  
    1.21    def formatted(input: XML.Body,
    1.22 -    margin: Double = margin_default,
    1.23 -    breakgain: Double = breakgain_default,
    1.24 -    metric: Metric = Metric_Default): XML.Body =
    1.25 +    margin: Double = default_margin,
    1.26 +    breakgain: Double = default_breakgain,
    1.27 +    metric: Metric = Default_Metric): XML.Body =
    1.28    {
    1.29      val emergencypos = (margin / 2).round.toInt
    1.30  
    1.31 @@ -180,8 +180,8 @@
    1.32    }
    1.33  
    1.34    def string_of(input: XML.Body,
    1.35 -      margin: Double = margin_default,
    1.36 -      breakgain: Double = breakgain_default,
    1.37 -      metric: Metric = Metric_Default): String =
    1.38 +      margin: Double = default_margin,
    1.39 +      breakgain: Double = default_breakgain,
    1.40 +      metric: Metric = Default_Metric): String =
    1.41      XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
    1.42  }