# HG changeset patch
# User wenzelm
# Date 1521303815 -3600
# Node ID 25e2b621bdcb0535a18721d69bdbf0251ad5f855
# Parent  4f383cd54f699771a69b16c569de0b2b996074c4
more interruptible use_theories;
tuned comments;

diff -r 4f383cd54f69 -r 25e2b621bdcb src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:13:27 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:23:35 2018 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/thy_resources.scala
     Author:     Makarius
 
-PIDE resources for theory files.
+PIDE resources for theory files: load/unload theories via PIDE document updates.
 */
 
 package isabelle
@@ -77,6 +77,10 @@
 
       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()
@@ -96,13 +100,17 @@
           case changed => if (dep_theories.exists(changed.nodes)) check_state
         }
 
-      session.commands_changed += consumer
-      check_state
-      result.join
-      session.commands_changed -= consumer
+      try {
+        session.commands_changed += consumer
+        check_state
+        result.join_result
+        session.commands_changed -= consumer
+      }
+      finally {
+        resources.unload_theories(session, id, dep_theories)
+      }
 
-      resources.unload_theories(session, id, dep_theories)
-
+      check_progress.cancel
       result.join
     }
   }