# HG changeset patch
# User wenzelm
# Date 1568628205 -7200
# Node ID 3f557ed88fd64b3ee0ede275f04b0dae9c4b498f
# Parent  374caac3d62437f80b33e794c46b3178e45b16bf
tuned message;

diff -r 374caac3d624 -r 3f557ed88fd6 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 16 12:03:25 2019 +0200
@@ -161,7 +161,7 @@
       def cancel_result: Use_Theories_State =
         if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt())))
 
-      def clean_theories: (List[Document.Node.Name], Use_Theories_State) =
+      def clean_theories: ((List[Document.Node.Name], Int), Use_Theories_State) =
       {
         @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
           : Set[Document.Node.Name] =
@@ -175,7 +175,7 @@
           }
         }
 
-        if (already_committed.isEmpty) (Nil, this)
+        if (already_committed.isEmpty) ((Nil, 0), this)
         else {
           val base =
             (for {
@@ -183,9 +183,9 @@
               if succs.isEmpty && already_committed.isDefinedAt(name)
             } yield name).toList
           val clean = frontier(base, Set.empty)
-          if (clean.isEmpty) (Nil, this)
+          if (clean.isEmpty) ((Nil, 0), this)
           else {
-            (dep_graph.topological_order.filter(clean),
+            ((dep_graph.topological_order.filter(clean), dep_graph.size - clean.size),
               copy(dep_graph = dep_graph.exclude(clean)))
           }
         }
@@ -323,9 +323,10 @@
 
         val delay_commit_clean =
           Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
-            val clean_theories = use_theories_state.change_result(_.clean_theories)
+            val (clean_theories, remaining) = use_theories_state.change_result(_.clean_theories)
             if (clean_theories.nonEmpty) {
-              progress.echo("Removing " + clean_theories.length + " theories ...")
+              progress.echo("Removing " + clean_theories.length +
+                " theories (" + remaining + " remaining) ...")
               resources.clean_theories(session, id, clean_theories)
             }
           }