# HG changeset patch
# User wenzelm
# Date 1521215054 -3600
# Node ID 812ed06dadecdbe762dea00a4648c2e764647136
# Parent  e59220a075dec219a2947889b609a03a37fc19fa
interruptible exploration of dependencies;

diff -r e59220a075de -r 812ed06dadec src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Mar 16 16:38:46 2018 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Mar 16 16:44:14 2018 +0100
@@ -297,7 +297,10 @@
     if (initiators.isEmpty) ""
     else "\n(required by " + show_path(initiators.reverse) + ")"
 
-  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+  private def require_thy(
+    progress: Progress,
+    initiators: List[Document.Node.Name],
+    required: Dependencies,
     thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, pos) = thy
@@ -313,11 +316,13 @@
       else {
         try {
           if (initiators.contains(name)) error(cycle_msg(initiators))
+
+          progress.expose_interrupt()
           val header =
             try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
             catch { case ERROR(msg) => cat_error(msg, message) }
           Document.Node.Entry(name, header) ::
-            require_thys(name :: initiators, required1, header.imports)
+            require_thys(progress, name :: initiators, required1, header.imports)
         }
         catch {
           case e: Throwable =>
@@ -327,10 +332,15 @@
     }
   }
 
-  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+  private def require_thys(
+      progress: Progress,
+      initiators: List[Document.Node.Name],
+      required: Dependencies,
       thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    (required /: thys)(require_thy(initiators, _, _))
+    (required /: thys)(require_thy(progress, initiators, _, _))
 
-  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    require_thys(Nil, Dependencies.empty, thys)
+  def dependencies(
+      thys: List[(Document.Node.Name, Position.T)],
+      progress: Progress = No_Progress): Dependencies =
+    require_thys(progress, Nil, Dependencies.empty, thys)
 }
diff -r e59220a075de -r 812ed06dadec src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 16 16:38:46 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 16:44:14 2018 +0100
@@ -66,10 +66,12 @@
     def use_theories(
       theories: List[(String, Position.T)],
       qualifier: String = Sessions.DRAFT,
-      master_dir: String = ""): Theories_Result =
+      master_dir: String = "",
+      progress: Progress = No_Progress): Theories_Result =
     {
       val requirements =
-        resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
+        resources.load_theories(session, theories, qualifier = qualifier,
+          master_dir = master_dir, progress = progress)
 
       val result = Future.promise[Theories_Result]
 
@@ -148,13 +150,14 @@
     session: Session,
     theories: List[(String, Position.T)],
     qualifier: String = Sessions.DRAFT,
-    master_dir: String = ""): List[Document.Node.Name] =
+    master_dir: String = "",
+    progress: Progress = No_Progress): List[Document.Node.Name] =
   {
     val import_names =
       for ((thy, pos) <- theories)
       yield (import_name(qualifier, master_dir, thy), pos)
 
-    val dependencies = resources.dependencies(import_names).check_errors
+    val dependencies = resources.dependencies(import_names, progress = progress).check_errors
     val loaded_theories = dependencies.theories.map(read_thy(_))
 
     val edits =