discontinued pointless option: timing is always on (overall theory only);
authorwenzelm
Fri Oct 31 18:56:59 2014 +0100 (2014-10-31)
changeset 58849ef7700ecce83
parent 58848 fd0c85d7da38
child 58850 1bb0ad7827b4
discontinued pointless option: timing is always on (overall theory only);
etc/options
src/HOL/ROOT
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/resources.ML
src/Pure/Tools/build.ML
     1.1 --- a/etc/options	Fri Oct 31 17:08:54 2014 +0100
     1.2 +++ b/etc/options	Fri Oct 31 18:56:59 2014 +0100
     1.3 @@ -90,9 +90,6 @@
     1.4  option condition : string = ""
     1.5    -- "required environment variables for subsequent theories (separated by commas)"
     1.6  
     1.7 -option timing : bool = false
     1.8 -  -- "global timing of toplevel command execution and theory processing"
     1.9 -
    1.10  option timeout : real = 0
    1.11    -- "timeout for session build job (seconds > 0)"
    1.12  
     2.1 --- a/src/HOL/ROOT	Fri Oct 31 17:08:54 2014 +0100
     2.2 +++ b/src/HOL/ROOT	Fri Oct 31 18:56:59 2014 +0100
     2.3 @@ -758,7 +758,7 @@
     2.4      Misc_Datatype
     2.5      Misc_Primcorec
     2.6      Misc_Primrec
     2.7 -  theories [condition = ISABELLE_FULL_TEST, timing]
     2.8 +  theories [condition = ISABELLE_FULL_TEST]
     2.9      Brackin
    2.10      IsaFoR
    2.11      Misc_N2M
    2.12 @@ -1098,6 +1098,6 @@
    2.13      Some benchmark on large record.
    2.14    *}
    2.15    options [document = false]
    2.16 -  theories [condition = ISABELLE_FULL_TEST, timing]
    2.17 +  theories [condition = ISABELLE_FULL_TEST]
    2.18      Record_Benchmark
    2.19  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Fri Oct 31 17:08:54 2014 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Oct 31 18:56:59 2014 +0100
     3.3 @@ -26,7 +26,6 @@
     3.4    val pretty_state: state -> Pretty.T list
     3.5    val print_state: state -> unit
     3.6    val pretty_abstract: state -> Pretty.T
     3.7 -  val timing: bool Unsynchronized.ref
     3.8    val profiling: int Unsynchronized.ref
     3.9    type transition
    3.10    val empty: transition
    3.11 @@ -211,7 +210,6 @@
    3.12  
    3.13  (** toplevel transitions **)
    3.14  
    3.15 -val timing = Unsynchronized.ref false;
    3.16  val profiling = Unsynchronized.ref 0;
    3.17  
    3.18  
     4.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 31 17:08:54 2014 +0100
     4.2 +++ b/src/Pure/PIDE/resources.ML	Fri Oct 31 18:56:59 2014 +0100
     4.3 @@ -151,8 +151,6 @@
     4.4  
     4.5  fun load_thy document last_timing update_time master_dir header text_pos text parents =
     4.6    let
     4.7 -    val time = ! Toplevel.timing;
     4.8 -
     4.9      val {name = (name, _), ...} = header;
    4.10      val _ = Thy_Header.define_keywords header;
    4.11  
    4.12 @@ -166,10 +164,9 @@
    4.13        |> Present.begin_theory update_time
    4.14            (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    4.15  
    4.16 -    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    4.17      val (results, thy) =
    4.18 -      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
    4.19 -    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    4.20 +      cond_timeit true ("theory " ^ quote name)
    4.21 +        (fn () => excursion master_dir last_timing init elements);
    4.22  
    4.23      fun present () =
    4.24        let
     5.1 --- a/src/Pure/Tools/build.ML	Fri Oct 31 17:08:54 2014 +0100
     5.2 +++ b/src/Pure/Tools/build.ML	Fri Oct 31 18:56:59 2014 +0100
     5.3 @@ -108,8 +108,7 @@
     5.4      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     5.5      |> Multithreading.max_threads_setmp (Options.int options "threads")
     5.6      |> Unsynchronized.setmp Future.ML_statistics true
     5.7 -    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     5.8 -    |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
     5.9 +    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin");
    5.10  
    5.11  fun use_theories_condition last_timing (options, thys) =
    5.12    let val condition = space_explode "," (Options.string options "condition") in