tuned signature;
authorwenzelm
Sat Sep 08 12:01:37 2018 +0200 (8 months ago)
changeset 68943e564605d4cac
parent 68942 4709898282a6
child 68944 ce68b1488612
tuned signature;
src/Pure/General/json.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/General/json.scala	Sat Sep 08 12:01:22 2018 +0200
     1.2 +++ b/src/Pure/General/json.scala	Sat Sep 08 12:01:37 2018 +0200
     1.3 @@ -309,6 +309,11 @@
     1.4            case _ => None
     1.5          }
     1.6      }
     1.7 +
     1.8 +    object Seconds {
     1.9 +      def unapply(json: T): Option[Time] =
    1.10 +        Double.unapply(json).map(Time.seconds(_))
    1.11 +    }
    1.12    }
    1.13  
    1.14  
    1.15 @@ -381,4 +386,9 @@
    1.16      list(obj, name, JSON.Value.String.unapply _)
    1.17    def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
    1.18      list_default(obj, name, JSON.Value.String.unapply _, default)
    1.19 +
    1.20 +  def seconds(obj: T, name: String): Option[Time] =
    1.21 +    value(obj, name, Value.Seconds.unapply)
    1.22 +  def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
    1.23 +    value_default(obj, name, Value.Seconds.unapply, default)
    1.24  }
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:22 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:37 2018 +0200
     2.3 @@ -78,9 +78,9 @@
     2.4        (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
     2.5    }
     2.6  
     2.7 -  val default_check_delay: Double = 0.5
     2.8 -  val default_nodes_status_delay: Double = -1.0
     2.9 -  val default_commit_clean_delay: Double = 60.0
    2.10 +  val default_check_delay = Time.seconds(0.5)
    2.11 +  val default_nodes_status_delay = Time.seconds(-1.0)
    2.12 +  val default_commit_clean_delay = Time.seconds(60.0)
    2.13  
    2.14  
    2.15    class Session private[Thy_Resources](
    2.16 @@ -194,14 +194,14 @@
    2.17        theories: List[String],
    2.18        qualifier: String = Sessions.DRAFT,
    2.19        master_dir: String = "",
    2.20 -      check_delay: Time = Time.seconds(default_check_delay),
    2.21 +      check_delay: Time = default_check_delay,
    2.22        check_limit: Int = 0,
    2.23        watchdog_timeout: Time = Time.zero,
    2.24 -      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
    2.25 +      nodes_status_delay: Time = default_nodes_status_delay,
    2.26        id: UUID = UUID(),
    2.27        // commit: must not block, must not fail
    2.28        commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
    2.29 -      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
    2.30 +      commit_clean_delay: Time = default_commit_clean_delay,
    2.31        progress: Progress = No_Progress): Theories_Result =
    2.32      {
    2.33        val dep_theories =
     3.1 --- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:22 2018 +0200
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:37 2018 +0200
     3.3 @@ -158,10 +158,10 @@
     3.4        pretty_margin: Double = Pretty.default_margin,
     3.5        unicode_symbols: Boolean = false,
     3.6        export_pattern: String = "",
     3.7 -      check_delay: Double = Thy_Resources.default_check_delay,
     3.8 +      check_delay: Time = Thy_Resources.default_check_delay,
     3.9        check_limit: Int = 0,
    3.10 -      watchdog_timeout: Double = 0.0,
    3.11 -      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
    3.12 +      watchdog_timeout: Time = Time.zero,
    3.13 +      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    3.14  
    3.15      def unapply(json: JSON.T): Option[Args] =
    3.16        for {
    3.17 @@ -171,11 +171,11 @@
    3.18          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    3.19          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    3.20          export_pattern <- JSON.string_default(json, "export_pattern")
    3.21 -        check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
    3.22 +        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    3.23          check_limit <- JSON.int_default(json, "check_limit")
    3.24 -        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
    3.25 +        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
    3.26          nodes_status_delay <-
    3.27 -          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    3.28 +          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    3.29        }
    3.30        yield {
    3.31          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    3.32 @@ -191,9 +191,9 @@
    3.33      {
    3.34        val result =
    3.35          session.use_theories(args.theories, master_dir = args.master_dir,
    3.36 -          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
    3.37 -          watchdog_timeout = Time.seconds(args.watchdog_timeout),
    3.38 -          nodes_status_delay = Time.seconds(args.nodes_status_delay),
    3.39 +          check_delay = args.check_delay, check_limit = args.check_limit,
    3.40 +          watchdog_timeout = args.watchdog_timeout,
    3.41 +          nodes_status_delay = args.nodes_status_delay,
    3.42            id = id, progress = progress)
    3.43  
    3.44        def output_text(s: String): String =