# HG changeset patch
# User wenzelm
# Date 1546087749 -3600
# Node ID 913970ae232464fe1d6cd1d05afca1011f0d218d
# Parent  1d2e6a4e073f30d1df3b7a256a0fb671c3184c0e
tuned, according to Isabelle/MMT;

diff -r 1d2e6a4e073f -r 913970ae2324 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Dec 29 13:15:13 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Dec 29 13:49:09 2018 +0100
@@ -17,7 +17,7 @@
     deps: Sessions.Deps,
     output_dir: Path,
     snapshot: Document.Snapshot,
-    node_status: Document_Status.Node_Status)
+    status: Document_Status.Node_Status)
   {
     def write(file_name: Path, bytes: Bytes)
     {
@@ -102,8 +102,8 @@
         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)
+              val (snapshot, status) = args
+              if (status.ok) consume(deps, snapshot, status)
               else {
                 consumer_ok.change(_ => false)
                 for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
@@ -114,8 +114,8 @@
               true
             })
 
-      def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
-        consumer.send((snapshot, node_status))
+      def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
+        consumer.send((snapshot, status))
 
       def shutdown(): Boolean =
       {
@@ -183,9 +183,9 @@
     def consume(
       deps: Sessions.Deps,
       snapshot: Document.Snapshot,
-      node_status: Document_Status.Node_Status)
+      status: Document_Status.Node_Status)
     {
-      val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
+      val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status)
       aspects.foreach(_.operation(aspect_args))
     }