src/Pure/Thy/thy_resources.scala

 {
   resources =>
 
   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,
     theories: List[(String, Position.T)],
     qualifier: String = Sessions.DRAFT,

       for ((thy, pos) <- theories)
       yield (import_name(qualifier, master_dir, thy), pos)
 
     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 =>
         {
           val st1 = st.insert_required(id, dep_theories)