# HG changeset patch
# User wenzelm
# Date 1536784406 -7200
# Node ID 807099160468d56092bb24ed87edcac755ee6b5e
# Parent  5717fbc555219b286d14fb770bc161fbbd3feea1# Parent  30daac7848b9f900892701e21ce1ae5fb4d5b60e
merged

diff -r 5717fbc55521 -r 807099160468 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Wed Sep 12 18:44:31 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 12 22:33:26 2018 +0200
@@ -80,7 +80,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_commit_cleanup_delay = Time.seconds(60.0)
   val default_watchdog_timeout = Time.seconds(600.0)
 
 
@@ -192,7 +192,7 @@
       id: UUID = UUID(),
       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
-      commit_clean_delay: Time = default_commit_clean_delay,
+      commit_cleanup_delay: Time = default_commit_cleanup_delay,
       progress: Progress = No_Progress): Theories_Result =
     {
       val dep_theories =
@@ -237,7 +237,7 @@
           }
 
         val delay_commit_clean =
-          Standard_Thread.delay_first(commit_clean_delay max Time.zero) {
+          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
             val clean = use_theories_state.value.already_committed.keySet
             resources.clean_theories(session, id, clean)
           }
@@ -281,7 +281,7 @@
 
               check_result()
 
-              if (commit.isDefined && commit_clean_delay > Time.zero) {
+              if (commit.isDefined && commit_cleanup_delay > Time.zero) {
                 if (use_theories_state.value.finished_result)
                   delay_commit_clean.revoke
                 else delay_commit_clean.invoke
diff -r 5717fbc55521 -r 807099160468 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Wed Sep 12 18:44:31 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Wed Sep 12 22:33:26 2018 +0200
@@ -92,7 +92,7 @@
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     verbose: Boolean = false,
-    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
+    commit_cleanup_delay: Time = Thy_Resources.default_commit_cleanup_delay,
     watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
@@ -164,7 +164,7 @@
       session.use_theories(use_theories,
         progress = progress,
         commit = Some(Consumer.apply _),
-        commit_clean_delay = commit_clean_delay,
+        commit_cleanup_delay = commit_cleanup_delay,
         watchdog_timeout = watchdog_timeout)
 
     val session_result = session.stop()
@@ -183,7 +183,7 @@
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
-      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
+      var commit_cleanup_delay = Thy_Resources.default_commit_cleanup_delay
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
       var requirements = false
@@ -205,7 +205,7 @@
     -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(Thy_Resources.default_commit_clean_delay) + """)
+      Value.Seconds(Thy_Resources.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
@@ -226,7 +226,7 @@
 """ + 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_clean_delay = Value.Seconds.parse(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),
@@ -253,7 +253,7 @@
             dirs = dirs,
             select_dirs = select_dirs,
             output_dir = output_dir,
-            commit_clean_delay = commit_clean_delay,
+            commit_cleanup_delay = commit_cleanup_delay,
             watchdog_timeout = watchdog_timeout,
             verbose = verbose,
             selection = Sessions.Selection(