src/Pure/Tools/dump.scala
changeset 68947 ea804c814693
parent 68946 6dd1460f6920
child 68948 9abd946f990c
     1.1 --- a/src/Pure/Tools/dump.scala	Sat Sep 08 13:22:23 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 08 13:36:40 2018 +0200
     1.3 @@ -76,8 +76,6 @@
     1.4    /* dump */
     1.5  
     1.6    val default_output_dir: Path = Path.explode("dump")
     1.7 -  val default_commit_clean_delay: Time = Time.seconds(-1.0)
     1.8 -  val default_watchdog_timeout: Time = Time.seconds(600.0)
     1.9  
    1.10    def make_options(options: Options, aspects: List[Aspect]): Options =
    1.11    {
    1.12 @@ -93,8 +91,8 @@
    1.13      select_dirs: List[Path] = Nil,
    1.14      output_dir: Path = default_output_dir,
    1.15      verbose: Boolean = false,
    1.16 -    commit_clean_delay: Time = default_commit_clean_delay,
    1.17 -    watchdog_timeout: Time = default_watchdog_timeout,
    1.18 +    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
    1.19 +    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
    1.20      system_mode: Boolean = false,
    1.21      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    1.22    {
    1.23 @@ -184,11 +182,11 @@
    1.24      {
    1.25        var aspects: List[Aspect] = known_aspects
    1.26        var base_sessions: List[String] = Nil
    1.27 -      var commit_clean_delay = default_commit_clean_delay
    1.28 +      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
    1.29        var select_dirs: List[Path] = Nil
    1.30        var output_dir = default_output_dir
    1.31        var requirements = false
    1.32 -      var watchdog_timeout = default_watchdog_timeout
    1.33 +      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
    1.34        var exclude_session_groups: List[String] = Nil
    1.35        var all_sessions = false
    1.36        var dirs: List[Path] = Nil
    1.37 @@ -205,13 +203,13 @@
    1.38    Options are:
    1.39      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    1.40      -B NAME      include session NAME and all descendants
    1.41 -    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
    1.42 -      Value.Seconds(default_commit_clean_delay) + """)
    1.43 +    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    1.44 +      Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
    1.45      -D DIR       include session directory and select its sessions
    1.46      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    1.47      -R           operate on requirements of selected sessions
    1.48 -    -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
    1.49 -      Value.Seconds(default_watchdog_timeout) + """)
    1.50 +    -W SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    1.51 +      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
    1.52      -X NAME      exclude sessions from group NAME and all descendants
    1.53      -a           select all sessions
    1.54      -d DIR       include session directory