support for watchdog_timeout;
authorwenzelm
Sat Sep 08 12:34:11 2018 +0200 (8 months ago)
changeset 68945fa5d936daf1c
parent 68944 ce68b1488612
child 68946 6dd1460f6920
support for watchdog_timeout;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Sat Sep 08 12:18:15 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 08 12:34:11 2018 +0200
     1.3 @@ -75,8 +75,9 @@
     1.4  
     1.5    /* dump */
     1.6  
     1.7 -  val default_output_dir = Path.explode("dump")
     1.8 -  val default_commit_clean_delay = Time.seconds(-1.0)
     1.9 +  val default_output_dir: Path = Path.explode("dump")
    1.10 +  val default_commit_clean_delay: Time = Time.seconds(-1.0)
    1.11 +  val default_watchdog_timeout: Time = Time.seconds(600.0)
    1.12  
    1.13    def make_options(options: Options, aspects: List[Aspect]): Options =
    1.14    {
    1.15 @@ -93,6 +94,7 @@
    1.16      output_dir: Path = default_output_dir,
    1.17      verbose: Boolean = false,
    1.18      commit_clean_delay: Time = default_commit_clean_delay,
    1.19 +    watchdog_timeout: Time = default_watchdog_timeout,
    1.20      system_mode: Boolean = false,
    1.21      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    1.22    {
    1.23 @@ -163,7 +165,8 @@
    1.24        session.use_theories(use_theories,
    1.25          progress = progress,
    1.26          commit = Some(Consumer.apply _),
    1.27 -        commit_clean_delay = commit_clean_delay)
    1.28 +        commit_clean_delay = commit_clean_delay,
    1.29 +        watchdog_timeout = watchdog_timeout)
    1.30  
    1.31      val session_result = session.stop()
    1.32  
    1.33 @@ -185,6 +188,7 @@
    1.34        var select_dirs: List[Path] = Nil
    1.35        var output_dir = default_output_dir
    1.36        var requirements = false
    1.37 +      var watchdog_timeout = default_watchdog_timeout
    1.38        var exclude_session_groups: List[String] = Nil
    1.39        var all_sessions = false
    1.40        var dirs: List[Path] = Nil
    1.41 @@ -206,6 +210,8 @@
    1.42      -D DIR       include session directory and select its sessions
    1.43      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    1.44      -R           operate on requirements of selected sessions
    1.45 +    -W SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
    1.46 +      default_commit_clean_delay.seconds.toInt + """)
    1.47      -X NAME      exclude sessions from group NAME and all descendants
    1.48      -a           select all sessions
    1.49      -d DIR       include session directory
    1.50 @@ -225,6 +231,7 @@
    1.51        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    1.52        "O:" -> (arg => output_dir = Path.explode(arg)),
    1.53        "R" -> (_ => requirements = true),
    1.54 +      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
    1.55        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    1.56        "a" -> (_ => all_sessions = true),
    1.57        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.58 @@ -254,6 +261,7 @@
    1.59              select_dirs = select_dirs,
    1.60              output_dir = output_dir,
    1.61              commit_clean_delay = commit_clean_delay,
    1.62 +            watchdog_timeout = watchdog_timeout,
    1.63              verbose = verbose,
    1.64              selection = Sessions.Selection(
    1.65                requirements = requirements,