more build options;
authorwenzelm
Tue Jul 24 21:54:49 2012 +0200 (2012-07-24)
changeset 4849203530cf284ca
parent 48491 6f2bcc0a16e0
child 48493 142ab4ff8fa8
more build options;
etc/options
src/HOL/ROOT
src/Pure/System/build.ML
     1.1 --- a/etc/options	Tue Jul 24 21:48:41 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 21:54:49 2012 +0200
     1.3 @@ -28,3 +28,5 @@
     1.4  declare names_short : bool = false
     1.5  declare names_unique : bool = true
     1.6  
     1.7 +declare timing : bool = false
     1.8 +
     2.1 --- a/src/HOL/ROOT	Tue Jul 24 21:48:41 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Jul 24 21:54:49 2012 +0200
     2.3 @@ -862,8 +862,7 @@
     2.4  session Datatype_Benchmark = HOL +
     2.5    description {* Some rather large datatype examples (from John Harrison). *}
     2.6    options [document = false]
     2.7 -  theories [condition = ISABELLE_BENCHMARK]
     2.8 -    (* FIXME Toplevel.timing := true; *)
     2.9 +  theories [condition = ISABELLE_BENCHMARK, timing]
    2.10      Brackin
    2.11      Instructions
    2.12      SML
    2.13 @@ -872,7 +871,6 @@
    2.14  session Record_Benchmark = HOL +
    2.15    description {* Some benchmark on large record. *}
    2.16    options [document = false]
    2.17 -  theories [condition = ISABELLE_BENCHMARK]
    2.18 -    (* FIXME Toplevel.timing := true; *)
    2.19 +  theories [condition = ISABELLE_BENCHMARK, timing]
    2.20      Record_Benchmark
    2.21  
     3.1 --- a/src/Pure/System/build.ML	Tue Jul 24 21:48:41 2012 +0200
     3.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 21:54:49 2012 +0200
     3.3 @@ -31,7 +31,8 @@
     3.4          (Options.bool options "show_question_marks")
     3.5      |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
     3.6      |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
     3.7 -    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique");
     3.8 +    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
     3.9 +    |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    3.10  
    3.11  fun use_theories (options, thys) =
    3.12    let val condition = space_explode "," (Options.string options "condition") in