src/Pure/Tools/dump.scala

--- a/src/Pure/Tools/dump.scala	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Dec 27 16:56:53 2018 +0100
@@ -94,8 +94,6 @@
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     verbose: Boolean = false,
-    commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
-    watchdog_timeout: Time = Headless.default_watchdog_timeout,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
   {
@@ -163,11 +161,7 @@
         include_sessions = include_sessions, progress = progress, log = log)
 
     val use_theories_result =
-      session.use_theories(use_theories,
-        progress = progress,
-        commit = Some(Consumer.apply _),
-        commit_cleanup_delay = commit_cleanup_delay,
-        watchdog_timeout = watchdog_timeout)
+      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
 
     session.stop()
 
@@ -189,11 +183,9 @@
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
-      var commit_cleanup_delay = Headless.default_commit_cleanup_delay
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
       var requirements = false
-      var watchdog_timeout = Headless.default_watchdog_timeout
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var dirs: List[Path] = Nil
@@ -210,13 +202,9 @@
   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 (0 = disabled, default: """ +
-      Value.Seconds(Headless.default_commit_cleanup_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   watchdog timeout for PIDE processing (0 = disabled, default: """ +
-      Value.Seconds(Headless.default_watchdog_timeout) + """)
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory
@@ -232,11 +220,9 @@
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
-      "C:" -> (arg => commit_cleanup_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))),
@@ -259,8 +245,6 @@
             dirs = dirs,
             select_dirs = select_dirs,
             output_dir = output_dir,
-            commit_cleanup_delay = commit_cleanup_delay,
-            watchdog_timeout = watchdog_timeout,
             verbose = verbose,
             selection = Sessions.Selection(
               requirements = requirements,