more accurate output;
authorwenzelm
Sat, 08 Sep 2018 13:22:23 +0200
changeset 68946 6dd1460f6920
parent 68945 fa5d936daf1c
child 68947 ea804c814693
more accurate output;
src/Pure/General/value.scala
src/Pure/Tools/dump.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))
--- a/src/Pure/Tools/dump.scala	Sat Sep 08 12:34:11 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 13:22:23 2018 +0200
@@ -206,12 +206,12 @@
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
     -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
-      default_commit_clean_delay.seconds.toInt + """)
+      Value.Seconds(default_commit_clean_delay) + """)
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
-    -W SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
-      default_commit_clean_delay.seconds.toInt + """)
+    -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
+      Value.Seconds(default_watchdog_timeout) + """)
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory