src/Pure/Tools/dump.scala

   def the_aspect(name: String): Aspect =
     known_aspects.find(aspect => aspect.name == name) getOrElse
       error("Unknown aspect " + quote(name))
 
 
+  /* session */
+
+  def session(dump_options: Options, logic: String,
+    consume: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
+    progress: Progress = No_Progress,
+    log: Logger = No_Logger,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    system_mode: Boolean = false,
+    selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
+  {
+    /* dependencies */
+
+    val deps =
+      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
+        selection_deps(selection)
+
+    val include_sessions =
+      deps.sessions_structure.imports_topological_order
+
+    val use_theories =
+      for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
+      yield name.theory
+
+
+    /* dump aspects asynchronously */
+
+    object Consumer
+    {
+      private val consumer_ok = Synchronized(true)
+
+      private val consumer =
+        Consumer_Thread.fork(name = "dump")(
+          consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
+            {
+              val (snapshot, node_status) = args
+              if (node_status.ok) consume(deps, snapshot, node_status)
+              else {
+                consumer_ok.change(_ => false)
+                for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
+                  val msg = XML.content(Pretty.formatted(List(tree)))
+                  progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg)
+                }
+              }
+              true
+            })
+
+      def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
+        consumer.send((snapshot, node_status))
+
+      def shutdown(): Boolean =
+      {
+        consumer.shutdown()
+        consumer_ok.value
+      }
+    }
+
+
+    /* run session */
+
+    val session =
+      Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
+        include_sessions = include_sessions, progress = progress, log = log)
+
+    val use_theories_result =
+      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
+
+    session.stop()
+
+    val consumer_ok = Consumer.shutdown()
+
+    use_theories_result.nodes_pending match {
+      case Nil =>
+      case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
+    }
+
+    use_theories_result.ok && consumer_ok
+  }
+
+
   /* dump */
 
   val default_output_dir: Path = Path.explode("dump")
 
-  def make_options(options: Options, aspects: List[Aspect]): Options =
+  def make_options(options: Options, aspects: List[Aspect] = Nil): Options =
   {
     val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
     val options1 =
       options0 + "completion_limit=0" + "ML_statistics=false" +
         "parallel_proofs=0" + "editor_tracing_messages=0"

     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
 
     val dump_options = make_options(options, aspects)
 
-
-    /* dependencies */
-
-    val deps =
-      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
-        selection_deps(selection)
-
-    val include_sessions =
-      deps.sessions_structure.imports_topological_order
-
-    val use_theories =
-      for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
-      yield name.theory
-
-
-    /* dump aspects asynchronously */
-
-    object Consumer
-    {
-      private val consumer_ok = Synchronized(true)
-
-      private val consumer =
-        Consumer_Thread.fork(name = "dump")(
-          consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
-            {
-              val (snapshot, node_status) = args
-              if (node_status.ok) {
-                val aspect_args =
-                  Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
-                aspects.foreach(_.operation(aspect_args))
-              }
-              else {
-                consumer_ok.change(_ => false)
-                for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
-                  val msg = XML.content(Pretty.formatted(List(tree)))
-                  progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg)
-                }
-              }
-              true
-            })
-
-      def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
-        consumer.send((snapshot, node_status))
-
-      def shutdown(): Boolean =
-      {
-        consumer.shutdown()
-        consumer_ok.value
-      }
-    }
-
-
-    /* session */
-
-    val session =
-      Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
-        include_sessions = include_sessions, progress = progress, log = log)
-
-    val use_theories_result =
-      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
-
-    session.stop()
-
-    val consumer_ok = Consumer.shutdown()
-
-    use_theories_result.nodes_pending match {
-      case Nil =>
-      case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
-    }
-
-    use_theories_result.ok && consumer_ok
+    def consume(
+      deps: Sessions.Deps,
+      snapshot: Document.Snapshot,
+      node_status: Document_Status.Node_Status)
+    {
+      val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
+      aspects.foreach(_.operation(aspect_args))
+    }
+
+    session(dump_options, logic, consume _,
+      progress = progress, log = log, dirs = dirs, select_dirs = select_dirs, selection = selection)
   }
 
 
   /* Isabelle tool wrapper */