# HG changeset patch
# User wenzelm
# Date 1357218224 -3600
# Node ID 49621c7550750d9b969c6fccd56738e3c0a1d930
# Parent  82e9178e6a9835e225db1b7939f77865d9be7024
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;

diff -r 82e9178e6a98 -r 49621c755075 etc/options
--- a/etc/options	Thu Jan 03 13:54:45 2013 +0100
+++ b/etc/options	Thu Jan 03 14:03:44 2013 +0100
@@ -53,8 +53,6 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_proofs_threshold : int = 100
   -- "threshold for sub-proof parallelization"
-option ML_statistics : bool = false
-  -- "ML runtime statistics of parallel execution environment"
 
 
 section "Detail of Proof Recording"
diff -r 82e9178e6a98 -r 49621c755075 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Jan 03 13:54:45 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 03 14:03:44 2013 +0100
@@ -238,7 +238,7 @@
   protocol_command "Isabelle_Process.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
-        Future.ML_statistics := Options.bool options "ML_statistics";
+        Future.ML_statistics := true;
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
         if Multithreading.max_threads_value () < 2
diff -r 82e9178e6a98 -r 49621c755075 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Jan 03 13:54:45 2013 +0100
+++ b/src/Pure/Tools/build.ML	Thu Jan 03 14:03:44 2013 +0100
@@ -43,7 +43,7 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
-    |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
+    |> Unsynchronized.setmp Future.ML_statistics true
     |> no_document options ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
diff -r 82e9178e6a98 -r 49621c755075 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 13:54:45 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 14:03:44 2013 +0100
@@ -43,7 +43,7 @@
   private val relevant_options =
     Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
       "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
-      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
+      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
       "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
       "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")