# HG changeset patch
# User wenzelm
# Date 1570371763 -7200
# Node ID 73514ccad7a61a18909c632f0778ba86c864f561
# Parent  89f6af1b483f97fef55f359fc7924ecb8c80a31b
clarified signature: read full session requirements;

diff -r 89f6af1b483f -r 73514ccad7a6 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Oct 06 15:28:59 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Oct 06 16:22:43 2019 +0200
@@ -23,8 +23,11 @@
       theory_graph.topological_order.flatMap(theory(_))
   }
 
-  def read_session(store: Sessions.Store,
+  def read_session(
+    store: Sessions.Store,
+    sessions_structure: Sessions.Structure,
     session_name: String,
+    progress: Progress = No_Progress,
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
@@ -38,17 +41,21 @@
     cache: Term.Cache = Term.make_cache()): Session =
   {
     val thys =
-      using(store.open_database(session_name))(db =>
-      {
-        db.transaction {
-          Export.read_theory_names(db, session_name).map((theory_name: String) =>
-            read_theory(Export.Provider.database(db, session_name, theory_name),
-              session_name, theory_name, types = types, consts = consts,
-              axioms = axioms, thms = thms, classes = classes, locales = locales,
-              locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
-              typedefs = typedefs, cache = Some(cache)))
-        }
-      })
+      sessions_structure.build_requirements(List(session_name)).flatMap(session =>
+        using(store.open_database(session))(db =>
+        {
+          db.transaction {
+            for (theory <- Export.read_theory_names(db, session))
+            yield {
+              progress.echo("Reading theory " + theory)
+              read_theory(Export.Provider.database(db, session, theory),
+                session, theory, types = types, consts = consts,
+                axioms = axioms, thms = thms, classes = classes, locales = locales,
+                locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
+                typedefs = typedefs, cache = Some(cache))
+            }
+          }
+        }))
 
     val graph0 =
       (Graph.string[Option[Theory]] /: thys) { case (g, thy) => g.new_node(thy.name, Some(thy)) }