src/Pure/Tools/dump.scala

       error("Unknown aspect " + quote(name))
 
 
   /* dump */
 
-  val default_output_dir = Path.explode("dump")
-  val default_commit_clean_delay = Time.seconds(-1.0)
+  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 =
   {
     val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })

     dirs: List[Path] = Nil,
     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,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
   {
     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")

 
     val theories_result =
       session.use_theories(use_theories,
         progress = progress,
         commit = Some(Consumer.apply _),
-        commit_clean_delay = commit_clean_delay)
+        commit_clean_delay = commit_clean_delay,
+        watchdog_timeout = watchdog_timeout)
 
     val session_result = session.stop()
 
     val consumer_ok = Consumer.shutdown()
 

       var base_sessions: List[String] = Nil
       var commit_clean_delay = 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 exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")

     -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
       default_commit_clean_delay.seconds.toInt + """)
     -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 (disabled for < 0, default: """ +
+      default_commit_clean_delay.seconds.toInt + """)
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory
     -g NAME      select session group NAME
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)

       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
+      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "l:" -> (arg => logic = arg),

             progress = progress,
             dirs = dirs,
             select_dirs = select_dirs,
             output_dir = output_dir,
             commit_clean_delay = commit_clean_delay,
+            watchdog_timeout = watchdog_timeout,
             verbose = verbose,
             selection = Sessions.Selection(
               requirements = requirements,
               all_sessions = all_sessions,
               base_sessions = base_sessions,