unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;

--- a/etc/options	Mon Oct 01 19:30:36 2018 +0200
+++ b/etc/options	Tue Oct 02 19:02:47 2018 +0200
@@ -174,7 +174,7 @@
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
-  -- "initial number of tracing messages for each command transaction"
+  -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"

--- a/src/Pure/System/isabelle_process.ML	Mon Oct 01 19:30:36 2018 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Oct 02 19:02:47 2018 +0200
@@ -71,7 +71,8 @@
           Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
-              val ok = n <= Options.default_int "editor_tracing_messages";
+              val limit = Options.default_int "editor_tracing_messages";
+              val ok = limit <= 0 orelse n <= limit;
             in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()

--- 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)(_ + _) })
   }