# HG changeset patch
# User wenzelm
# Date 1343159689 -7200
# Node ID 03530cf284ca6407011139dc22f30b4fd60cc2b1
# Parent  6f2bcc0a16e067d55b8d63a3399e4714a5adab86
more build options;

diff -r 6f2bcc0a16e0 -r 03530cf284ca etc/options
--- 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
+
diff -r 6f2bcc0a16e0 -r 03530cf284ca src/HOL/ROOT
--- 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
 
diff -r 6f2bcc0a16e0 -r 03530cf284ca src/Pure/System/build.ML
--- 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