# HG changeset patch
# User wenzelm
# Date 1521307813 -3600
# Node ID fee080c4045fa34d48a8ac49d080664f4c156e16
# Parent  c854e50c211402cd0898a12e590d0b9286d9146e
more robust check_state loop, even without session activity (e.g. idempotent use_theories);

diff -r c854e50c2114 -r fee080c4045f src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:18:53 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:30:13 2018 +0100
@@ -77,10 +77,6 @@
 
       val result = Future.promise[Theories_Result]
 
-      val check_progress =
-        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
-          { if (progress.stopped) result.cancel }
-
       def check_state
       {
         val state = session.current_state()
@@ -95,6 +91,10 @@
         }
       }
 
+      val check_progress =
+        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
+          { if (progress.stopped) result.cancel else check_state }
+
       val consumer =
         Session.Consumer[Session.Commands_Changed](getClass.getName) {
           case changed => if (dep_theories.exists(changed.nodes)) check_state
@@ -102,15 +102,14 @@
 
       try {
         session.commands_changed += consumer
-        check_state
         result.join_result
+        check_progress.cancel
         session.commands_changed -= consumer
       }
       finally {
         resources.unload_theories(session, id, dep_theories)
       }
 
-      check_progress.cancel
       result.join
     }
   }