more generous tracing_limit, with explicit system option;
authorwenzelm
Sun Nov 18 16:04:13 2012 +0100 (2012-11-18 ago)
changeset 501195c370a036de7
parent 50118 89a14e495526
child 50120 245f5947233c
more generous tracing_limit, with explicit system option;
NEWS
etc/options
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/src/isabelle_options.scala
     1.1 --- a/NEWS	Sun Nov 18 15:38:37 2012 +0100
     1.2 +++ b/NEWS	Sun Nov 18 16:04:13 2012 +0100
     1.3 @@ -60,9 +60,9 @@
     1.4  
     1.5  * Smarter handling of tracing messages: output window informs about
     1.6  accumulated messages; prover transactions are limited to emit maximum
     1.7 -amount of output, before being canceled (cf. tracing_limit option).
     1.8 -This avoids swamping the front-end with potentially infinite message
     1.9 -streams.
    1.10 +amount of output, before being canceled (cf. system option
    1.11 +"editor_tracing_limit").  This avoids swamping the front-end with
    1.12 +potentially infinite message streams.
    1.13  
    1.14  * More plugin options and preferences, based on Isabelle/Scala.  The
    1.15  jEdit plugin option panel provides access to some Isabelle/Scala
     2.1 --- a/etc/options	Sun Nov 18 15:38:37 2012 +0100
     2.2 +++ b/etc/options	Sun Nov 18 16:04:13 2012 +0100
     2.3 @@ -97,3 +97,6 @@
     2.4  
     2.5  option editor_reparse_limit : int = 10000
     2.6    -- "maximum amount of reparsed text outside perspective"
     2.7 +
     2.8 +option editor_tracing_limit : int = 1000000
     2.9 +  -- "maximum tracing volume for each command transaction"
     3.1 --- a/src/Pure/System/isabelle_process.ML	Sun Nov 18 15:38:37 2012 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Nov 18 16:04:13 2012 +0100
     3.3 @@ -65,7 +65,7 @@
     3.4  
     3.5  (* tracing limit *)
     3.6  
     3.7 -val tracing_limit = Unsynchronized.ref 500000;
     3.8 +val tracing_limit = Unsynchronized.ref 1000000;
     3.9  
    3.10  val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
    3.11  
    3.12 @@ -224,7 +224,8 @@
    3.13          if Multithreading.max_threads_value () < 2
    3.14          then Multithreading.max_threads := 2 else ();
    3.15          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
    3.16 -        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold"
    3.17 +        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
    3.18 +        tracing_limit := Options.int options "editor_tracing_limit"
    3.19        end);
    3.20  
    3.21  end;
     4.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 15:38:37 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 16:04:13 2012 +0100
     4.3 @@ -44,7 +44,8 @@
     4.4      Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
     4.5        "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
     4.6        "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
     4.7 -      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
     4.8 +      "editor_input_delay", "editor_output_delay", "editor_reparse_limit", "editor_tracing_limit",
     4.9 +      "editor_update_delay")
    4.10  
    4.11    relevant_options.foreach(Isabelle.options.value.check_name _)
    4.12