# HG changeset patch
# User wenzelm
# Date 1527683683 -7200
# Node ID d7920eb7de54d490ca3bd7ad4a811af3a827dace
# Parent  88c07fabd5b411422dba001138ac334c426a1fdd
report theory progress via PIDE node status;

diff -r 88c07fabd5b4 -r d7920eb7de54 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue May 29 22:29:32 2018 +0200
+++ b/src/Pure/System/progress.scala	Wed May 30 14:34:43 2018 +0200
@@ -51,7 +51,10 @@
   }
 
   override def theory(session: String, theory: String): Unit =
-    if (verbose) echo(session + ": theory " + theory)
+    if (verbose) {
+      if (session == "") echo("theory " + theory)
+      else echo(session + ": theory " + theory)
+    }
 
   @volatile private var is_stopped = false
   override def interrupt_handler[A](e: => A): A =
diff -r 88c07fabd5b4 -r d7920eb7de54 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue May 29 22:29:32 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Wed May 30 14:34:43 2018 +0200
@@ -144,9 +144,32 @@
         Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
           { if (progress.stopped) result.cancel else check_state }
 
+      val theories_progress = Synchronized(Set.empty[Document.Node.Name])
+
       val consumer =
         Session.Consumer[Session.Commands_Changed](getClass.getName) {
-          case changed => if (dep_theories.exists(changed.nodes)) check_state
+          case changed =>
+            if (dep_theories.exists(changed.nodes)) {
+
+              val check_theories =
+                (for (command <- changed.commands.iterator if command.potentially_initialized)
+                  yield command.node_name).toSet
+
+              if (check_theories.nonEmpty) {
+                val snapshot = session.snapshot()
+                val initialized =
+                  theories_progress.change_result(theories =>
+                  {
+                    val initialized =
+                      (check_theories -- theories).toList.filter(name =>
+                        Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
+                    (initialized, theories ++ initialized)
+                  })
+                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
+              }
+
+              check_state
+            }
         }
 
       try {
diff -r 88c07fabd5b4 -r d7920eb7de54 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue May 29 22:29:32 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Wed May 30 14:34:43 2018 +0200
@@ -31,10 +31,6 @@
 
   private val known_aspects =
     List(
-      Aspect("list", "list theory nodes",
-        { case args =>
-            for (node_name <- args.result.node_names) args.progress.echo(node_name.toString)
-        }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {