# HG changeset patch
# User wenzelm
# Date 1536065987 -7200
# Node ID a9deff1bcb65f6c9b9224615c3b53e562cc87945
# Parent  90a6b714aca34978d993fd6e242358be76b469b2
tuned;

diff -r 90a6b714aca3 -r a9deff1bcb65 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:50:52 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:59:47 2018 +0200
@@ -152,14 +152,15 @@
           }
       }
 
-      val theories_progress = Synchronized(Set.empty[Document.Node.Name])
+      val consumer =
+      {
+        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
 
-      val delay_nodes_status =
-        Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
-          progress.nodes_status(current_nodes_status.value)
-        }
+        val delay_nodes_status =
+          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
+            progress.nodes_status(current_nodes_status.value)
+          }
 
-      val consumer =
         Session.Consumer[Session.Commands_Changed](getClass.getName) {
           case changed =>
             if (changed.nodes.exists(dep_theories_set)) {
@@ -217,6 +218,7 @@
               check_state()
             }
         }
+      }
 
       try {
         session.commands_changed += consumer