# HG changeset patch
# User wenzelm
# Date 1536406600 -7200
# Node ID ea804c814693935a768bf6dcb3c0eb4c4db3f917
# Parent  6dd1460f6920d0a9f2f3fd0a0a7708477306b018
clarified defaults;
more uniform treatment of "disabled" case;

diff -r 6dd1460f6920 -r ea804c814693 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Sep 08 13:22:23 2018 +0200
+++ b/src/Doc/System/Server.thy	Sat Sep 08 13:36:40 2018 +0200
@@ -909,7 +909,7 @@
   \quad~~\<open>export_pattern?: string,\<close> \\
   \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
   \quad~~\<open>check_limit?: int,\<close> \\
-  \quad~~\<open>watchdog_timeout?: double,\<close> \\
+  \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
   \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
   \end{tabular}
 
diff -r 6dd1460f6920 -r ea804c814693 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 13:22:23 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 13:36:40 2018 +0200
@@ -81,6 +81,7 @@
   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)
+  val default_watchdog_timeout = Time.seconds(600.0)
 
 
   class Session private[Thy_Resources](
@@ -196,7 +197,7 @@
       master_dir: String = "",
       check_delay: Time = default_check_delay,
       check_limit: Int = 0,
-      watchdog_timeout: Time = Time.zero,
+      watchdog_timeout: Time = default_watchdog_timeout,
       nodes_status_delay: Time = default_nodes_status_delay,
       id: UUID = UUID(),
       // commit: must not block, must not fail
@@ -303,7 +304,7 @@
 
               check_result()
 
-              if (commit.isDefined && commit_clean_delay >= Time.zero) {
+              if (commit.isDefined && commit_clean_delay > Time.zero) {
                 if (use_theories_state.value.finished_result)
                   delay_commit_clean.revoke
                 else delay_commit_clean.invoke
diff -r 6dd1460f6920 -r ea804c814693 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Sep 08 13:22:23 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 13:36:40 2018 +0200
@@ -76,8 +76,6 @@
   /* dump */
 
   val default_output_dir: Path = Path.explode("dump")
-  val default_commit_clean_delay: Time = Time.seconds(-1.0)
-  val default_watchdog_timeout: Time = Time.seconds(600.0)
 
   def make_options(options: Options, aspects: List[Aspect]): Options =
   {
@@ -93,8 +91,8 @@
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     verbose: Boolean = false,
-    commit_clean_delay: Time = default_commit_clean_delay,
-    watchdog_timeout: Time = default_watchdog_timeout,
+    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
+    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
   {
@@ -184,11 +182,11 @@
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
-      var commit_clean_delay = default_commit_clean_delay
+      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
       var requirements = false
-      var watchdog_timeout = default_watchdog_timeout
+      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var dirs: List[Path] = Nil
@@ -205,13 +203,13 @@
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
-    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
-      Value.Seconds(default_commit_clean_delay) + """)
+    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
+      Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
-    -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
-      Value.Seconds(default_watchdog_timeout) + """)
+    -W SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
+      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory
diff -r 6dd1460f6920 -r ea804c814693 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:22:23 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:36:40 2018 +0200
@@ -160,7 +160,7 @@
       export_pattern: String = "",
       check_delay: Time = Thy_Resources.default_check_delay,
       check_limit: Int = 0,
-      watchdog_timeout: Time = Time.zero,
+      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
       nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
 
     def unapply(json: JSON.T): Option[Args] =
@@ -173,7 +173,8 @@
         export_pattern <- JSON.string_default(json, "export_pattern")
         check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
         check_limit <- JSON.int_default(json, "check_limit")
-        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
+        watchdog_timeout <-
+          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
         nodes_status_delay <-
           JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
       }