# 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