# HG changeset patch
# User wenzelm
# Date 1545927340 -3600
# Node ID 9403ff523825fda4a4cd428c02d35b16293b9b4a
# Parent  9457d85204f51aee773214be02e0969a0ee9262a
tuned signature: for other dump-like tools;

diff -r 9457d85204f5 -r 9403ff523825 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Dec 27 16:59:55 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Dec 27 17:15:40 2018 +0100
@@ -73,35 +73,17 @@
       error("Unknown aspect " + quote(name))
 
 
-  /* dump */
-
-  val default_output_dir: Path = Path.explode("dump")
+  /* session */
 
-  def make_options(options: Options, aspects: List[Aspect]): 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"
-    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
-  }
-
-  def dump(options: Options, logic: String,
-    aspects: List[Aspect] = Nil,
+  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,
-    output_dir: Path = default_output_dir,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
   {
-    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 =
@@ -127,11 +109,7 @@
           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))
-              }
+              if (node_status.ok) consume(deps, snapshot, node_status)
               else {
                 consumer_ok.change(_ => false)
                 for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
@@ -153,7 +131,7 @@
     }
 
 
-    /* session */
+    /* run session */
 
     val session =
       Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
@@ -175,6 +153,48 @@
   }
 
 
+  /* dump */
+
+  val default_output_dir: Path = Path.explode("dump")
+
+  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"
+    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+  }
+
+  def dump(options: Options, logic: String,
+    aspects: List[Aspect] = Nil,
+    progress: Progress = No_Progress,
+    log: Logger = No_Logger,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    output_dir: Path = default_output_dir,
+    system_mode: Boolean = false,
+    selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
+  {
+    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)
+
+    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 */
 
   val isabelle_tool =