X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaInit.ml;h=26f4b40ffe421a1867b85e6358137ea5730ae187;hb=6ad533c972e6c9e9db53f38f972e7c0792160f2e;hp=06f7815b912e3669e6004855445e4fa47cbd8f2d;hpb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;p=helm.git diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 06f7815b9..26f4b40ff 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - type thingsToInitilaize = ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry @@ -45,13 +43,14 @@ let already_configured s l = let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ - "db.nodb", "false"; - "matita.debug", "false"; - "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; - "matita.profile", "true"; - "matita.system", "false"; - "matita.verbosity", "1"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.profile", "true"; + "matita.system", "false"; + "matita.verbosity", "1"; + "matita.bench", "false"; + "matita.paste_unicode_as_tex", "false" (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is * intuitively verbose *) ] @@ -67,7 +66,6 @@ let fill_registry init_status = init_status let load_configuration init_status = - wants [ Registry ] init_status; if not (already_configured [ConfigurationFile] init_status) then begin Helm_registry.load_from !conffile; @@ -75,6 +73,17 @@ let load_configuration init_status = let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in Helm_registry.set "user.name" login end; + let home = Helm_registry.get_string "matita.basedir" in + let user_conf_file = home ^ "/matita.conf.xml" in + if HExtlib.is_regular user_conf_file then + begin + HLog.message ("Loading additional conf file from " ^ user_conf_file); + try + Helm_registry.load_from user_conf_file + with exn -> + HLog.error + ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn)) + end; ConfigurationFile::init_status end else @@ -126,42 +135,49 @@ let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) [ "matitac", - sprintf "MatitaC v%s + Printf.sprintf "MatitaC v%s Usage: matitac [ OPTION ... ] FILE Options:" BuildTimeConf.version; "gragrep", - sprintf "Grafite Grep v%s + Printf.sprintf "Grafite Grep v%s Usage: gragrep [ -r ] PATH +Options:" + BuildTimeConf.version; + "matitaprover", + Printf.sprintf "Matita's prover v%s +Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", - sprintf "Matita v%s + Printf.sprintf "Matita v%s Usage: matita [ OPTION ... ] [ FILE ... ] Options:" BuildTimeConf.version; "cicbrowser", - sprintf + Printf.sprintf "CIC Browser v%s Usage: cicbrowser [ URL | WHELP QUERY ] Options:" BuildTimeConf.version; "matitadep", - sprintf "MatitaDep v%s + Printf.sprintf "MatitaDep v%s Usage: matitadep [ OPTION ... ] FILE ... Options:" BuildTimeConf.version; "matitaclean", - sprintf "MatitaClean v%s + Printf.sprintf "MatitaClean v%s Usage: matitaclean all matitaclean [ (FILE | URI) ... ] Options:" BuildTimeConf.version; "matitamake", - sprintf "MatitaMake v%s + Printf.sprintf "MatitaMake v%s 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 @@ -193,7 +209,8 @@ Options:" BuildTimeConf.version; ] let default_usage = - sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version + Printf.sprintf + "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version let usage () = let basename = Filename.basename Sys.argv.(0) in @@ -207,9 +224,15 @@ 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 ] + wants [Registry] init_status; + let includes = ref [] in + let default_includes = [ + "."; + BuildTimeConf.stdlib_dir_devel; + BuildTimeConf.stdlib_dir_installed ; ] + in + let absolutize s = + if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s in let args = ref [] in let add_l l = fun s -> l := s :: !l in @@ -231,12 +254,15 @@ let parse_cmdline init_status = "-force", Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true), ("Force actions that would not be executed per default"); - "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true), - ("Avoid using external database connection" - ^ "\n WARNING: disable many features"); "-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"; @@ -253,19 +279,30 @@ let parse_cmdline init_status = Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true), ("Do not catch top-level exception " ^ "(useful for backtrace inspection)"); + "-onepass", + Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true), + "Enable only one disambiguation pass"; ] else [] in std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs in let set_list ~key l = - Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l) + Helm_registry.set_list Helm_registry.of_string ~key ~value:l in Arg.parse arg_spec (add_l args) (usage ()); + let includes = + List.map absolutize ((List.rev !includes) @ default_includes) in set_list ~key:"matita.includes" includes; + let args = List.rev (List.filter (fun x -> x <> "") !args) in 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 @@ -274,11 +311,16 @@ let die_usage () = print_endline (usage ()); exit 1 +let conf_components = + [ load_configuration; fill_registry; parse_cmdline] + +let other_components = + [ initialize_makelib; initialize_db; initialize_environment ] + let initialize_all () = status := List.fold_left (fun s f -> f s) !status - [ fill_registry; parse_cmdline; load_configuration; initialize_makelib; - initialize_db; initialize_environment ] + (conf_components @ other_components) (* initialize_notation (initialize_environment (initialize_db @@ -286,14 +328,9 @@ let initialize_all () = (load_configuration (parse_cmdline !status))))) *) -let load_configuration_file () = - status := load_configuration !status - -let parse_cmdline () = - status := parse_cmdline !status +let parse_cmdline_and_configuration_file () = + status := List.fold_left (fun s f -> f s) !status conf_components -let fill_registry () = - status := fill_registry !status ;; Inversion_principle.init ()