# HG changeset patch
# User wenzelm
# Date 1536400897 -7200
# Node ID e564605d4cacca00c23561a4aaa5e8fa1ed752cf
# Parent  4709898282a613069a0fa71fa419aeb0bd09187c
tuned signature;

diff -r 4709898282a6 -r e564605d4cac src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Sat Sep 08 12:01:22 2018 +0200
+++ b/src/Pure/General/json.scala	Sat Sep 08 12:01:37 2018 +0200
@@ -309,6 +309,11 @@
           case _ => None
         }
     }
+
+    object Seconds {
+      def unapply(json: T): Option[Time] =
+        Double.unapply(json).map(Time.seconds(_))
+    }
   }
 
 
@@ -381,4 +386,9 @@
     list(obj, name, JSON.Value.String.unapply _)
   def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
     list_default(obj, name, JSON.Value.String.unapply _, default)
+
+  def seconds(obj: T, name: String): Option[Time] =
+    value(obj, name, Value.Seconds.unapply)
+  def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
+    value_default(obj, name, Value.Seconds.unapply, default)
 }
diff -r 4709898282a6 -r e564605d4cac src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:22 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:37 2018 +0200
@@ -78,9 +78,9 @@
       (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
   }
 
-  val default_check_delay: Double = 0.5
-  val default_nodes_status_delay: Double = -1.0
-  val default_commit_clean_delay: Double = 60.0
+  val default_check_delay = Time.seconds(0.5)
+  val default_nodes_status_delay = Time.seconds(-1.0)
+  val default_commit_clean_delay = Time.seconds(60.0)
 
 
   class Session private[Thy_Resources](
@@ -194,14 +194,14 @@
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
-      check_delay: Time = Time.seconds(default_check_delay),
+      check_delay: Time = default_check_delay,
       check_limit: Int = 0,
       watchdog_timeout: Time = Time.zero,
-      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
+      nodes_status_delay: Time = default_nodes_status_delay,
       id: UUID = UUID(),
       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
-      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
+      commit_clean_delay: Time = default_commit_clean_delay,
       progress: Progress = No_Progress): Theories_Result =
     {
       val dep_theories =
diff -r 4709898282a6 -r e564605d4cac src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:22 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 12:01:37 2018 +0200
@@ -158,10 +158,10 @@
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false,
       export_pattern: String = "",
-      check_delay: Double = Thy_Resources.default_check_delay,
+      check_delay: Time = Thy_Resources.default_check_delay,
       check_limit: Int = 0,
-      watchdog_timeout: Double = 0.0,
-      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
+      watchdog_timeout: Time = Time.zero,
+      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -171,11 +171,11 @@
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
         export_pattern <- JSON.string_default(json, "export_pattern")
-        check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
+        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
         check_limit <- JSON.int_default(json, "check_limit")
-        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
+        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
         nodes_status_delay <-
-          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
+          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
       }
       yield {
         Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
@@ -191,9 +191,9 @@
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
-          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
-          watchdog_timeout = Time.seconds(args.watchdog_timeout),
-          nodes_status_delay = Time.seconds(args.nodes_status_delay),
+          check_delay = args.check_delay, check_limit = args.check_limit,
+          watchdog_timeout = args.watchdog_timeout,
+          nodes_status_delay = args.nodes_status_delay,
           id = id, progress = progress)
 
       def output_text(s: String): String =