src/Pure/General/value.scala
changeset 68946 6dd1460f6920
parent 68944 ce68b1488612
child 69450 b28b001e7ee8
     1.1 --- a/src/Pure/General/value.scala	Sat Sep 08 12:34:11 2018 +0200
     1.2 +++ b/src/Pure/General/value.scala	Sat Sep 08 13:22:23 2018 +0200
     1.3 @@ -54,7 +54,11 @@
     1.4  
     1.5    object Seconds
     1.6    {
     1.7 -    def apply(x: Time): java.lang.String = x.toString
     1.8 +    def apply(t: Time): java.lang.String =
     1.9 +    {
    1.10 +      val s = t.seconds
    1.11 +      if (s.toInt.toDouble == s) s.toInt.toString else t.toString
    1.12 +    }
    1.13      def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
    1.14      def parse(s: java.lang.String): Time =
    1.15        unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))