--- a/etc/options Tue Jul 24 21:48:41 2012 +0200
+++ b/etc/options Tue Jul 24 21:54:49 2012 +0200
@@ -28,3 +28,5 @@
declare names_short : bool = false
declare names_unique : bool = true
+declare timing : bool = false
+
--- a/src/HOL/ROOT Tue Jul 24 21:48:41 2012 +0200
+++ b/src/HOL/ROOT Tue Jul 24 21:54:49 2012 +0200
@@ -862,8 +862,7 @@
session Datatype_Benchmark = HOL +
description {* Some rather large datatype examples (from John Harrison). *}
options [document = false]
- theories [condition = ISABELLE_BENCHMARK]
- (* FIXME Toplevel.timing := true; *)
+ theories [condition = ISABELLE_BENCHMARK, timing]
Brackin
Instructions
SML
@@ -872,7 +871,6 @@
session Record_Benchmark = HOL +
description {* Some benchmark on large record. *}
options [document = false]
- theories [condition = ISABELLE_BENCHMARK]
- (* FIXME Toplevel.timing := true; *)
+ theories [condition = ISABELLE_BENCHMARK, timing]
Record_Benchmark
--- a/src/Pure/System/build.ML Tue Jul 24 21:48:41 2012 +0200
+++ b/src/Pure/System/build.ML Tue Jul 24 21:54:49 2012 +0200
@@ -31,7 +31,8 @@
(Options.bool options "show_question_marks")
|> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
|> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
- |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique");
+ |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
+ |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
fun use_theories (options, thys) =
let val condition = space_explode "," (Options.string options "condition") in