--- a/src/Pure/Tools/dump.scala Mon Oct 01 19:30:36 2018 +0200
+++ b/src/Pure/Tools/dump.scala Tue Oct 02 19:02:47 2018 +0200
@@ -80,7 +80,9 @@
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"
+ val options1 =
+ options0 + "completion_limit=0" + "ML_statistics=false" +
+ "parallel_proofs=0" + "editor_tracing_messages=0"
(options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
}