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