# HG changeset patch
# User wenzelm
# Date 1521299885 -3600
# Node ID 3bf62a6e50e748b4858437275daeb241dd85a3da
# Parent  a4d5342898b1cda3a79e32625adb25bb01a720ff
more interruptible;
tuned signature;

diff -r a4d5342898b1 -r 3bf62a6e50e7 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:08:10 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:18:05 2018 +0100
@@ -169,16 +169,6 @@
 
   private val state = Synchronized(Thy_Resources.State())
 
-  def load_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
-  {
-    val path = node_name.path
-    if (!node_name.is_theory) error("Not a theory file: " + path)
-
-    val text = File.read(path)
-    val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
-    new Thy_Resources.Theory(node_name, node_header, text, true)
-  }
-
   def load_theories(
     session: Session,
     id: UUID,
@@ -193,7 +183,18 @@
 
     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
     val dep_theories = dependencies.theories
-    val loaded_theories = dep_theories.map(load_thy(_))
+
+    val loaded_theories =
+      for (node_name <- dep_theories)
+      yield {
+        val path = node_name.path
+        if (!node_name.is_theory) error("Not a theory file: " + path)
+
+        progress.expose_interrupt()
+        val text = File.read(path)
+        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
+        new Thy_Resources.Theory(node_name, node_header, text, true)
+      }
 
     val edits =
       state.change_result(st =>