tuned;
authorwenzelm
Tue, 04 Sep 2018 14:59:47 +0200
changeset 68906 a9deff1bcb65
parent 68905 90a6b714aca3
child 68907 3afa4f03864b
tuned;
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