src/Pure/Tools/server_commands.scala
changeset 68943 e564605d4cac
parent 68908 abc338d25640
child 68947 ea804c814693
     1.1 --- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:22 2018 +0200
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:37 2018 +0200
     1.3 @@ -158,10 +158,10 @@
     1.4        pretty_margin: Double = Pretty.default_margin,
     1.5        unicode_symbols: Boolean = false,
     1.6        export_pattern: String = "",
     1.7 -      check_delay: Double = Thy_Resources.default_check_delay,
     1.8 +      check_delay: Time = Thy_Resources.default_check_delay,
     1.9        check_limit: Int = 0,
    1.10 -      watchdog_timeout: Double = 0.0,
    1.11 -      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
    1.12 +      watchdog_timeout: Time = Time.zero,
    1.13 +      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    1.14  
    1.15      def unapply(json: JSON.T): Option[Args] =
    1.16        for {
    1.17 @@ -171,11 +171,11 @@
    1.18          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    1.19          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    1.20          export_pattern <- JSON.string_default(json, "export_pattern")
    1.21 -        check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
    1.22 +        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    1.23          check_limit <- JSON.int_default(json, "check_limit")
    1.24 -        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
    1.25 +        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
    1.26          nodes_status_delay <-
    1.27 -          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    1.28 +          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    1.29        }
    1.30        yield {
    1.31          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    1.32 @@ -191,9 +191,9 @@
    1.33      {
    1.34        val result =
    1.35          session.use_theories(args.theories, master_dir = args.master_dir,
    1.36 -          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
    1.37 -          watchdog_timeout = Time.seconds(args.watchdog_timeout),
    1.38 -          nodes_status_delay = Time.seconds(args.nodes_status_delay),
    1.39 +          check_delay = args.check_delay, check_limit = args.check_limit,
    1.40 +          watchdog_timeout = args.watchdog_timeout,
    1.41 +          nodes_status_delay = args.nodes_status_delay,
    1.42            id = id, progress = progress)
    1.43  
    1.44        def output_text(s: String): String =