# HG changeset patch
# User wenzelm
# Date 1571079604 -7200
# Node ID 4c8e28dabbc45b90670a0eebb1f6b9ae6c6d0a2d
# Parent  209327bd3e3ee14b7ea97a512d5a1261fa06a695
clarified signature;

diff -r 209327bd3e3e -r 4c8e28dabbc4 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 14 20:29:19 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 14 21:00:04 2019 +0200
@@ -97,35 +97,6 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def used_theories_condition(default_options: Options,
-      restrict: String => Boolean = _ => true,
-      progress: Progress = No_Progress)
-      : List[(Document.Node.Name, Options)] =
-    {
-      val default_skip_proofs = default_options.bool("skip_proofs")
-      for {
-        session_name <- sessions_structure.imports_graph.restrict(restrict).topological_order
-        entry @ (name, options) <- session_bases(session_name).used_theories
-        if {
-          def warn(msg: String): Unit =
-            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
-
-          val conditions =
-            space_explode(',', options.string("condition")).
-              filter(cond => Isabelle_System.getenv(cond) == "")
-          if (conditions.nonEmpty) {
-            warn("undefined " + conditions.mkString(", "))
-            false
-          }
-          else if (default_skip_proofs && !options.bool("skip_proofs")) {
-            warn("option skip_proofs")
-            false
-          }
-          else true
-        }
-      } yield entry
-    }
-
     def sources(name: String): List[SHA1.Digest] =
       session_bases(name).sources.map(_._2)
 
diff -r 209327bd3e3e -r 4c8e28dabbc4 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 20:29:19 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 21:00:04 2019 +0200
@@ -177,32 +177,52 @@
   }
 
   class Session private[Dump](
-    val context: Context, val logic: String, log: Logger, val selected_sessions: List[String])
+    val context: Context,
+    val logic: String,
+    log: Logger,
+    selected_sessions: List[String])
   {
     /* resources */
 
     def options: Options = context.session_options
 
-    private def progress: Progress = context.progress
+    private def deps = context.deps
+    private def progress = context.progress
 
     private val selected_session = selected_sessions.toSet
 
     private def selected_theory(name: Document.Node.Name): Boolean =
-      selected_session(context.deps.sessions_structure.theory_qualifier(name.theory))
+      selected_session(deps.sessions_structure.theory_qualifier(name.theory))
 
     val resources: Headless.Resources =
       Headless.Resources.make(options, logic, progress = progress, log = log,
         session_dirs = context.session_dirs,
-        include_sessions = context.deps.sessions_structure.imports_topological_order)
+        include_sessions = deps.sessions_structure.imports_topological_order)
 
     val used_theories: List[Document.Node.Name] =
     {
       for {
-        (name, _) <-
-          context.deps.used_theories_condition(options,
-            restrict = selected_session,
-            progress = progress)
+        session_name <-
+          deps.sessions_structure.imports_graph.restrict(selected_session).topological_order
+        (name, theory_options) <- deps(session_name).used_theories
         if !resources.session_base.loaded_theory(name.theory)
+        if {
+          def warn(msg: String): Unit =
+            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
+
+          val conditions =
+            space_explode(',', theory_options.string("condition")).
+              filter(cond => Isabelle_System.getenv(cond) == "")
+          if (conditions.nonEmpty) {
+            warn("undefined " + conditions.mkString(", "))
+            false
+          }
+          else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) {
+            warn("option skip_proofs")
+            false
+          }
+          else true
+        }
       } yield name
     }