tuned;

--- a/src/Pure/Tools/dump.scala	Fri Apr 03 20:27:52 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Apr 03 20:29:54 2020 +0200
@@ -106,9 +106,9 @@
         val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
         val options1 =
           options0 +
-            "completion_limit=0" +
             "ML_statistics=false" +
             "parallel_proofs=0" +
+            "completion_limit=0" +
             "editor_tracing_messages=0" +
             "editor_presentation"
         (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })