--- 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