# HG changeset patch
# User wenzelm
# Date 1535984606 -7200
# Node ID 1dbdad1b57a505e23b46cd59652d25649c04cf78
# Parent  58bf801d679a9edffe8913f1a36f43d915ac8850
more robust: load_theories after consumer is installed;

diff -r 58bf801d679a -r 1dbdad1b57a5 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Mon Sep 03 15:35:38 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Mon Sep 03 16:23:26 2018 +0200
@@ -107,8 +107,12 @@
       progress: Progress = No_Progress): Theories_Result =
     {
       val dep_theories =
-        resources.load_theories(session, id, theories, qualifier = qualifier,
-          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
+      {
+        val master = proper_string(master_dir) getOrElse tmp_dir_name
+        val import_names =
+          theories.map(thy => resources.import_name(qualifier, master, thy) -> Position.none)
+        resources.dependencies(import_names, progress = progress).check_errors.theories
+      }
       val dep_theories_set = dep_theories.toSet
 
       val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
@@ -202,6 +206,7 @@
 
       try {
         session.commands_changed += consumer
+        resources.load_theories(session, id, dep_theories, progress)
         result.join_result
         check_progress.cancel
         session.commands_changed -= consumer
@@ -306,14 +311,9 @@
   def load_theories(
     session: Session,
     id: UUID,
-    theories: List[String],
-    qualifier: String,
-    master_dir: String,
-    progress: Progress): List[Document.Node.Name] =
+    dep_theories: List[Document.Node.Name],
+    progress: Progress)
   {
-    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
-    val dependencies = resources.dependencies(import_names, progress = progress).check_errors
-    val dep_theories = dependencies.theories
 
     val loaded_theories =
       for (node_name <- dep_theories)
@@ -341,8 +341,6 @@
         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
         st1.update_theories(theory_edits.map(_._2))
       })
-
-    dep_theories
   }
 
   def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])