# HG changeset patch
# User wenzelm
# Date 1571077357 -7200
# Node ID 4739030a5bf224f0dad72b22fd60b706cfb827fa
# Parent  e94fec16bf50b00abd5e911abbe80e7fe9494f29
clarified signature;

diff -r e94fec16bf50 -r 4739030a5bf2 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 20:05:16 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 20:22:37 2019 +0200
@@ -177,11 +177,12 @@
   }
 
   class Session private[Dump](
-    context: Context, val logic: String, log: Logger, val selected_sessions: List[String])
+    val context: Context, val logic: String, log: Logger, val selected_sessions: List[String])
   {
     /* resources */
 
-    private val progress = context.progress
+    def options: Options = context.session_options
+    def progress: Progress = context.progress
 
     private val selected_session = selected_sessions.toSet
 
@@ -189,7 +190,7 @@
       selected_session(context.deps.sessions_structure.theory_qualifier(name.theory))
 
     val resources: Headless.Resources =
-      Headless.Resources.make(context.session_options, logic, progress = progress, log = log,
+      Headless.Resources.make(options, logic, progress = progress, log = log,
         session_dirs = context.session_dirs,
         include_sessions = context.deps.sessions_structure.imports_topological_order)
 
@@ -197,7 +198,7 @@
     {
       for {
         (name, _) <-
-          context.deps.used_theories_condition(context.session_options,
+          context.deps.used_theories_condition(options,
             restrict = selected_session,
             progress = progress)
         if !resources.session_base.loaded_theory(name.theory)
@@ -319,14 +320,16 @@
 
     context.build_logic(logic)
 
-    context.sessions(logic = logic, log = log).foreach(_.process((args: Args) =>
-      {
-        progress.echo("Processing theory " + args.print_node + " ...")
-        val aspect_args =
-          Aspect_Args(context.session_options, context.deps, progress, output_dir,
-            args.snapshot, args.status)
-        aspects.foreach(_.operation(aspect_args))
-      }))
+    for (session <- context.sessions(logic = logic, log = log)) {
+      session.process((args: Args) =>
+        {
+          progress.echo("Processing theory " + args.print_node + " ...")
+          val aspect_args =
+            Aspect_Args(session.options, context.deps, progress, output_dir,
+              args.snapshot, args.status)
+          aspects.foreach(_.operation(aspect_args))
+        })
+    }
   }