# HG changeset patch
# User wenzelm
# Date 1353251053 -3600
# Node ID 5c370a036de7f63ac3a538ded3479b7f3dad9ecd
# Parent  89a14e4955266bd6b63cd2082a1029b9c0ca1a1d
more generous tracing_limit, with explicit system option;

diff -r 89a14e495526 -r 5c370a036de7 NEWS
--- a/NEWS	Sun Nov 18 15:38:37 2012 +0100
+++ b/NEWS	Sun Nov 18 16:04:13 2012 +0100
@@ -60,9 +60,9 @@
 
 * Smarter handling of tracing messages: output window informs about
 accumulated messages; prover transactions are limited to emit maximum
-amount of output, before being canceled (cf. tracing_limit option).
-This avoids swamping the front-end with potentially infinite message
-streams.
+amount of output, before being canceled (cf. system option
+"editor_tracing_limit").  This avoids swamping the front-end with
+potentially infinite message streams.
 
 * More plugin options and preferences, based on Isabelle/Scala.  The
 jEdit plugin option panel provides access to some Isabelle/Scala
diff -r 89a14e495526 -r 5c370a036de7 etc/options
--- a/etc/options	Sun Nov 18 15:38:37 2012 +0100
+++ b/etc/options	Sun Nov 18 16:04:13 2012 +0100
@@ -97,3 +97,6 @@
 
 option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
+
+option editor_tracing_limit : int = 1000000
+  -- "maximum tracing volume for each command transaction"
diff -r 89a14e495526 -r 5c370a036de7 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun Nov 18 15:38:37 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sun Nov 18 16:04:13 2012 +0100
@@ -65,7 +65,7 @@
 
 (* tracing limit *)
 
-val tracing_limit = Unsynchronized.ref 500000;
+val tracing_limit = Unsynchronized.ref 1000000;
 
 val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
 
@@ -224,7 +224,8 @@
         if Multithreading.max_threads_value () < 2
         then Multithreading.max_threads := 2 else ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
-        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold"
+        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
+        tracing_limit := Options.int options "editor_tracing_limit"
       end);
 
 end;
diff -r 89a14e495526 -r 5c370a036de7 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 15:38:37 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 16:04:13 2012 +0100
@@ -44,7 +44,8 @@
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
       "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
       "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
-      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
+      "editor_input_delay", "editor_output_delay", "editor_reparse_limit", "editor_tracing_limit",
+      "editor_update_delay")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)