tuned signature;
authorwenzelm
Mon Mar 25 10:37:38 2013 +0100 (2013-03-25)
changeset 51507ebd5366e7a42
parent 51505 9e91959a8cfc
child 51508 48a1e09120d4
tuned signature;
src/Pure/General/pretty.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Pure/General/pretty.scala	Sun Mar 24 16:19:54 2013 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Mon Mar 25 10:37:38 2013 +0100
     1.3 @@ -31,14 +31,12 @@
     1.4    abstract class Metric
     1.5    {
     1.6      val unit: Double
     1.7 -    def average: Double
     1.8      def apply(s: String): Double
     1.9    }
    1.10  
    1.11    object Metric_Default extends Metric
    1.12    {
    1.13      val unit = 1.0
    1.14 -    val average = 1.0
    1.15      def apply(s: String): Double = s.length.toDouble
    1.16    }
    1.17  
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Mar 24 16:19:54 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Mar 25 10:37:38 2013 +0100
     2.3 @@ -168,7 +168,7 @@
     2.4    // NB: last line lacks \n
     2.5    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
     2.6    {
     2.7 -    val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
     2.8 +    val metric = pretty_metric(text_area.getPainter)
     2.9      val char_width = (metric.unit * metric.average).round.toInt
    2.10  
    2.11      val buffer = text_area.getBuffer
    2.12 @@ -208,14 +208,19 @@
    2.13  
    2.14    /* pretty text metric */
    2.15  
    2.16 -  def string_width(painter: TextAreaPainter, s: String): Double =
    2.17 -    painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
    2.18 +  abstract class Pretty_Metric extends Pretty.Metric
    2.19 +  {
    2.20 +    def average: Double
    2.21 +  }
    2.22  
    2.23 -  def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
    2.24 -    new Pretty.Metric {
    2.25 -      val unit = string_width(painter, Pretty.space)
    2.26 -      val average = string_width(painter, "mix") / (3 * unit)
    2.27 -      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit
    2.28 +  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
    2.29 +    new Pretty_Metric {
    2.30 +      def string_width(s: String): Double =
    2.31 +        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
    2.32 +
    2.33 +      val unit = string_width(Pretty.space)
    2.34 +      val average = string_width("mix") / (3 * unit)
    2.35 +      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
    2.36      }
    2.37  }
    2.38