# HG changeset patch
# User wenzelm
# Date 1414778219 -3600
# Node ID ef7700ecce838841eea74e3697fd8ae04ab289fb
# Parent  fd0c85d7da38ed5e1ba378ef0d870d67525db88e
discontinued pointless option: timing is always on (overall theory only);

diff -r fd0c85d7da38 -r ef7700ecce83 etc/options
--- a/etc/options	Fri Oct 31 17:08:54 2014 +0100
+++ b/etc/options	Fri Oct 31 18:56:59 2014 +0100
@@ -90,9 +90,6 @@
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
-option timing : bool = false
-  -- "global timing of toplevel command execution and theory processing"
-
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
diff -r fd0c85d7da38 -r ef7700ecce83 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Oct 31 17:08:54 2014 +0100
+++ b/src/HOL/ROOT	Fri Oct 31 18:56:59 2014 +0100
@@ -758,7 +758,7 @@
     Misc_Datatype
     Misc_Primcorec
     Misc_Primrec
-  theories [condition = ISABELLE_FULL_TEST, timing]
+  theories [condition = ISABELLE_FULL_TEST]
     Brackin
     IsaFoR
     Misc_N2M
@@ -1098,6 +1098,6 @@
     Some benchmark on large record.
   *}
   options [document = false]
-  theories [condition = ISABELLE_FULL_TEST, timing]
+  theories [condition = ISABELLE_FULL_TEST]
     Record_Benchmark
 
diff -r fd0c85d7da38 -r ef7700ecce83 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Oct 31 17:08:54 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Oct 31 18:56:59 2014 +0100
@@ -26,7 +26,6 @@
   val pretty_state: state -> Pretty.T list
   val print_state: state -> unit
   val pretty_abstract: state -> Pretty.T
-  val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
@@ -211,7 +210,6 @@
 
 (** toplevel transitions **)
 
-val timing = Unsynchronized.ref false;
 val profiling = Unsynchronized.ref 0;
 
 
diff -r fd0c85d7da38 -r ef7700ecce83 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Oct 31 17:08:54 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Oct 31 18:56:59 2014 +0100
@@ -151,8 +151,6 @@
 
 fun load_thy document last_timing update_time master_dir header text_pos text parents =
   let
-    val time = ! Toplevel.timing;
-
     val {name = (name, _), ...} = header;
     val _ = Thy_Header.define_keywords header;
 
@@ -166,10 +164,9 @@
       |> Present.begin_theory update_time
           (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
-    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
     val (results, thy) =
-      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
-    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
+      cond_timeit true ("theory " ^ quote name)
+        (fn () => excursion master_dir last_timing init elements);
 
     fun present () =
       let
diff -r fd0c85d7da38 -r ef7700ecce83 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Oct 31 17:08:54 2014 +0100
+++ b/src/Pure/Tools/build.ML	Fri Oct 31 18:56:59 2014 +0100
@@ -108,8 +108,7 @@
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Multithreading.max_threads_setmp (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
-    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
-    |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
+    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin");
 
 fun use_theories_condition last_timing (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in