src/Pure/Tools/dump.scala

   /* aspects */
 
   sealed case class Aspect_Args(
     options: Options,
     progress: Progress,
+    output_dir: Path,
     deps: Sessions.Deps,
-    output_dir: Path,
     snapshot: Document.Snapshot,
     status: Document_Status.Node_Status)
   {
     def write(file_name: Path, bytes: Bytes)
     {

   }
 
 
   /* session */
 
+  sealed case class Args(
+    deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status)
+  {
+    def print_node: String = snapshot.node_name.toString
+
+    def aspect_args(options: Options, progress: Progress, output_dir: Path): Aspect_Args =
+      Aspect_Args(options, progress, output_dir, deps, snapshot, status)
+  }
+
   def session(
     deps: Sessions.Deps,
     resources: Headless.Resources,
-    process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
+    process_theory: Args => Unit,
     progress: Progress = No_Progress)
   {
     /* asynchronous consumer */
 
     object Consumer

           consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
             {
               val (snapshot, status) = args
               val name = snapshot.node_name
               if (status.ok) {
-                try { process_theory(deps, snapshot, status) }
+                try { process_theory(Args(deps, snapshot, status)) }
                 catch {
                   case exn: Throwable if !Exn.is_interrupt(exn) =>
                   val msg = Exn.message(exn)
                   progress.echo("FAILED to process theory " + name)
                   progress.echo_error_message(msg)

       Headless.Resources.make(dump_options, logic, progress = progress, log = log,
         session_dirs = dirs ::: select_dirs,
         include_sessions = deps.sessions_structure.imports_topological_order)
 
     session(deps, resources, progress = progress,
-      process_theory =
-        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
+      process_theory = (args: Args) =>
         {
-          progress.echo("Processing theory " + snapshot.node_name + " ...")
-
-          val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status)
+          progress.echo("Processing theory " + args.print_node + " ...")
+
+          val aspect_args = args.aspect_args(dump_options, progress, output_dir)
           aspects.foreach(_.operation(aspect_args))
         })
   }