src/Pure/General/pretty.scala
changeset 51507 ebd5366e7a42
parent 51493 59d8a1031c00
child 51568 cdb4b7dc76cb
     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