--- 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