src/Pure/General/value.scala

--- a/src/Pure/General/value.scala	Sat Sep 08 12:34:11 2018 +0200
+++ b/src/Pure/General/value.scala	Sat Sep 08 13:22:23 2018 +0200
@@ -54,7 +54,11 @@
 
   object Seconds
   {
-    def apply(x: Time): java.lang.String = x.toString
+    def apply(t: Time): java.lang.String =
+    {
+      val s = t.seconds
+      if (s.toInt.toDouble == s) s.toInt.toString else t.toString
+    }
     def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
     def parse(s: java.lang.String): Time =
       unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))