always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
authorwenzelm
Thu Jan 03 14:03:44 2013 +0100 (2013-01-03)
changeset 5069849621c755075
parent 50697 82e9178e6a98
child 50699 373093ffcbda
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
etc/options
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.ML
src/Tools/jEdit/src/isabelle_options.scala
     1.1 --- a/etc/options	Thu Jan 03 13:54:45 2013 +0100
     1.2 +++ b/etc/options	Thu Jan 03 14:03:44 2013 +0100
     1.3 @@ -53,8 +53,6 @@
     1.4    -- "level of parallel proof checking: 0, 1, 2"
     1.5  option parallel_proofs_threshold : int = 100
     1.6    -- "threshold for sub-proof parallelization"
     1.7 -option ML_statistics : bool = false
     1.8 -  -- "ML runtime statistics of parallel execution environment"
     1.9  
    1.10  
    1.11  section "Detail of Proof Recording"
     2.1 --- a/src/Pure/System/isabelle_process.ML	Thu Jan 03 13:54:45 2013 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Jan 03 14:03:44 2013 +0100
     2.3 @@ -238,7 +238,7 @@
     2.4    protocol_command "Isabelle_Process.options"
     2.5      (fn [options_yxml] =>
     2.6        let val options = Options.decode (YXML.parse_body options_yxml) in
     2.7 -        Future.ML_statistics := Options.bool options "ML_statistics";
     2.8 +        Future.ML_statistics := true;
     2.9          Multithreading.trace := Options.int options "threads_trace";
    2.10          Multithreading.max_threads := Options.int options "threads";
    2.11          if Multithreading.max_threads_value () < 2
     3.1 --- a/src/Pure/Tools/build.ML	Thu Jan 03 13:54:45 2013 +0100
     3.2 +++ b/src/Pure/Tools/build.ML	Thu Jan 03 14:03:44 2013 +0100
     3.3 @@ -43,7 +43,7 @@
     3.4          (Options.int options "parallel_proofs_threshold")
     3.5      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     3.6      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     3.7 -    |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
     3.8 +    |> Unsynchronized.setmp Future.ML_statistics true
     3.9      |> no_document options ? Present.no_document
    3.10      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    3.11      |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
     4.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 13:54:45 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 14:03:44 2013 +0100
     4.3 @@ -43,7 +43,7 @@
     4.4    private val relevant_options =
     4.5      Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
     4.6        "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
     4.7 -      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
     4.8 +      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
     4.9        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
    4.10        "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
    4.11