X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaInit.ml;h=5866b74d8bff14c73e1d80ea9ccb58ac334453e1;hb=f520a046799605f705d0b37ef325ad73744c1afe;hp=06f7815b912e3669e6004855445e4fa47cbd8f2d;hpb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;p=helm.git diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 06f7815b9..5866b74d8 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -52,6 +52,7 @@ let registry_defaults = [ "matita.profile", "true"; "matita.system", "false"; "matita.verbosity", "1"; + "matita.bench", "false"; (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is * intuitively verbose *) ] @@ -162,6 +163,8 @@ Options:" Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) init Parameters: name (the name of the development, required) + root (the directory in which the delopment is rooted, + optional, default is current working directory) Description: tells matitamake that a new development radicated in the current working directory should be handled. clean @@ -208,8 +211,8 @@ let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs let parse_cmdline init_status = if not (already_configured [CmdLine] init_status) then begin let includes = ref [ - BuildTimeConf.stdlib_dir_installed ; - BuildTimeConf.stdlib_dir_devel ] + BuildTimeConf.stdlib_dir_devel; + BuildTimeConf.stdlib_dir_installed ; ] in let args = ref [] in let add_l l = fun s -> l := s :: !l in @@ -237,6 +240,12 @@ let parse_cmdline init_status = "-noprofile", Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), "Turns off profiling printings"; + "-profile-only", + Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), + "Activates only profiler with label matching the provided regex"; + "-bench", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true), + "Turns on parsable output on stdout, that is timings for matitac..."; "-preserve", Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), "Turns off automatic baseuri cleaning"; @@ -263,9 +272,15 @@ let parse_cmdline init_status = in Arg.parse arg_spec (add_l args) (usage ()); set_list ~key:"matita.includes" includes; + args := List.filter (fun x -> x <> "") !args; set_list ~key:"matita.args" args; HExtlib.set_profiling_printings - (fun () -> Helm_registry.get_bool "matita.profile"); + (fun s -> + Helm_registry.get_bool "matita.profile" && + Pcre.pmatch + ~pat:(Helm_registry.get_opt_default + Helm_registry.string ~default:".*" "matita.profile_only") + s); CmdLine :: init_status end else init_status