clarified defaults;
authorwenzelm
Sat Sep 08 13:36:40 2018 +0200 (8 months ago)
changeset 68947ea804c814693
parent 68946 6dd1460f6920
child 68948 9abd946f990c
clarified defaults;
more uniform treatment of "disabled" case;
src/Doc/System/Server.thy
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Sat Sep 08 13:22:23 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Sat Sep 08 13:36:40 2018 +0200
     1.3 @@ -909,7 +909,7 @@
     1.4    \quad~~\<open>export_pattern?: string,\<close> \\
     1.5    \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
     1.6    \quad~~\<open>check_limit?: int,\<close> \\
     1.7 -  \quad~~\<open>watchdog_timeout?: double,\<close> \\
     1.8 +  \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
     1.9    \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
    1.10    \end{tabular}
    1.11  
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 13:22:23 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 13:36:40 2018 +0200
     2.3 @@ -81,6 +81,7 @@
     2.4    val default_check_delay = Time.seconds(0.5)
     2.5    val default_nodes_status_delay = Time.seconds(-1.0)
     2.6    val default_commit_clean_delay = Time.seconds(60.0)
     2.7 +  val default_watchdog_timeout = Time.seconds(600.0)
     2.8  
     2.9  
    2.10    class Session private[Thy_Resources](
    2.11 @@ -196,7 +197,7 @@
    2.12        master_dir: String = "",
    2.13        check_delay: Time = default_check_delay,
    2.14        check_limit: Int = 0,
    2.15 -      watchdog_timeout: Time = Time.zero,
    2.16 +      watchdog_timeout: Time = default_watchdog_timeout,
    2.17        nodes_status_delay: Time = default_nodes_status_delay,
    2.18        id: UUID = UUID(),
    2.19        // commit: must not block, must not fail
    2.20 @@ -303,7 +304,7 @@
    2.21  
    2.22                check_result()
    2.23  
    2.24 -              if (commit.isDefined && commit_clean_delay >= Time.zero) {
    2.25 +              if (commit.isDefined && commit_clean_delay > Time.zero) {
    2.26                  if (use_theories_state.value.finished_result)
    2.27                    delay_commit_clean.revoke
    2.28                  else delay_commit_clean.invoke
     3.1 --- a/src/Pure/Tools/dump.scala	Sat Sep 08 13:22:23 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 08 13:36:40 2018 +0200
     3.3 @@ -76,8 +76,6 @@
     3.4    /* dump */
     3.5  
     3.6    val default_output_dir: Path = Path.explode("dump")
     3.7 -  val default_commit_clean_delay: Time = Time.seconds(-1.0)
     3.8 -  val default_watchdog_timeout: Time = Time.seconds(600.0)
     3.9  
    3.10    def make_options(options: Options, aspects: List[Aspect]): Options =
    3.11    {
    3.12 @@ -93,8 +91,8 @@
    3.13      select_dirs: List[Path] = Nil,
    3.14      output_dir: Path = default_output_dir,
    3.15      verbose: Boolean = false,
    3.16 -    commit_clean_delay: Time = default_commit_clean_delay,
    3.17 -    watchdog_timeout: Time = default_watchdog_timeout,
    3.18 +    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
    3.19 +    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
    3.20      system_mode: Boolean = false,
    3.21      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    3.22    {
    3.23 @@ -184,11 +182,11 @@
    3.24      {
    3.25        var aspects: List[Aspect] = known_aspects
    3.26        var base_sessions: List[String] = Nil
    3.27 -      var commit_clean_delay = default_commit_clean_delay
    3.28 +      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
    3.29        var select_dirs: List[Path] = Nil
    3.30        var output_dir = default_output_dir
    3.31        var requirements = false
    3.32 -      var watchdog_timeout = default_watchdog_timeout
    3.33 +      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
    3.34        var exclude_session_groups: List[String] = Nil
    3.35        var all_sessions = false
    3.36        var dirs: List[Path] = Nil
    3.37 @@ -205,13 +203,13 @@
    3.38    Options are:
    3.39      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    3.40      -B NAME      include session NAME and all descendants
    3.41 -    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
    3.42 -      Value.Seconds(default_commit_clean_delay) + """)
    3.43 +    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    3.44 +      Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
    3.45      -D DIR       include session directory and select its sessions
    3.46      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    3.47      -R           operate on requirements of selected sessions
    3.48 -    -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
    3.49 -      Value.Seconds(default_watchdog_timeout) + """)
    3.50 +    -W SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    3.51 +      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
    3.52      -X NAME      exclude sessions from group NAME and all descendants
    3.53      -a           select all sessions
    3.54      -d DIR       include session directory
     4.1 --- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:22:23 2018 +0200
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 13:36:40 2018 +0200
     4.3 @@ -160,7 +160,7 @@
     4.4        export_pattern: String = "",
     4.5        check_delay: Time = Thy_Resources.default_check_delay,
     4.6        check_limit: Int = 0,
     4.7 -      watchdog_timeout: Time = Time.zero,
     4.8 +      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     4.9        nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    4.10  
    4.11      def unapply(json: JSON.T): Option[Args] =
    4.12 @@ -173,7 +173,8 @@
    4.13          export_pattern <- JSON.string_default(json, "export_pattern")
    4.14          check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    4.15          check_limit <- JSON.int_default(json, "check_limit")
    4.16 -        watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout")
    4.17 +        watchdog_timeout <-
    4.18 +          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
    4.19          nodes_status_delay <-
    4.20            JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    4.21        }