tuned signature;
authorwenzelm
Sat Sep 08 12:18:15 2018 +0200 (10 months ago)
changeset 68944ce68b1488612
parent 68943 e564605d4cac
child 68945 fa5d936daf1c
tuned signature;
src/Pure/General/value.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/General/value.scala	Sat Sep 08 12:01:37 2018 +0200
     1.2 +++ b/src/Pure/General/value.scala	Sat Sep 08 12:18:15 2018 +0200
     1.3 @@ -51,4 +51,12 @@
     1.4      def parse(s: java.lang.String): scala.Double =
     1.5        unapply(s) getOrElse error("Bad real: " + quote(s))
     1.6    }
     1.7 +
     1.8 +  object Seconds
     1.9 +  {
    1.10 +    def apply(x: Time): java.lang.String = x.toString
    1.11 +    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
    1.12 +    def parse(s: java.lang.String): Time =
    1.13 +      unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
    1.14 +  }
    1.15  }
     2.1 --- a/src/Pure/Tools/dump.scala	Sat Sep 08 12:01:37 2018 +0200
     2.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 08 12:18:15 2018 +0200
     2.3 @@ -221,7 +221,7 @@
     2.4  """ + Library.prefix_lines("    ", show_aspects) + "\n",
     2.5        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
     2.6        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
     2.7 -      "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
     2.8 +      "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
     2.9        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.10        "O:" -> (arg => output_dir = Path.explode(arg)),
    2.11        "R" -> (_ => requirements = true),