# 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~~\export_pattern?: string,\ \\ \quad~~\check_delay?: double,\ & \<^bold>\default:\ \<^verbatim>\0.5\ \\ \quad~~\check_limit?: int,\ \\ - \quad~~\watchdog_timeout?: double,\ \\ + \quad~~\watchdog_timeout?: double,\ & \<^bold>\default:\ \<^verbatim>\600.0\ \\ \quad~~\nodes_status_delay?: double}\ & \<^bold>\default:\ \<^verbatim>\-1.0\ \\ \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) }