# HG changeset patch
# User wenzelm
# Date 1546085713 -3600
# Node ID 1d2e6a4e073f30d1df3b7a256a0fb671c3184c0e
# Parent  e2edf24b960e592691dc9d46680208d2abba4874
clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;

diff -r e2edf24b960e -r 1d2e6a4e073f src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Dec 29 12:52:58 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Dec 29 13:15:13 2018 +0100
@@ -55,14 +55,14 @@
         { case args =>
             for (entry <- args.snapshot.exports if entry.name == "document.tex")
               args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("editor_presentation", "export_document")),
+        }, options = List("export_document")),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {
               entry <- args.snapshot.exports
               if entry.name.startsWith(Export_Theory.export_prefix)
             } args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("editor_presentation", "export_theory"))
+        }, options = List("export_theory"))
     ).sortBy(_.name)
 
   def show_aspects: String =
@@ -161,7 +161,7 @@
     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"
+        "parallel_proofs=0" + "editor_tracing_messages=0" + "editor_presentation"
     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
   }