X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=8f3071334e7496c9b0bf9fd276353e859e6026b5;hb=892992b24f5476c2b4eed13f64e04854ef919020;hp=7ffb67d9f8cf8d15413f8ec2a7b2e438e04d9dc8;hpb=cb06122ec0250d63b18629e4a85f0515831114ce;p=helm.git diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 7ffb67d9f..8f3071334 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - type thingsToInitilaize = ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry @@ -52,13 +50,17 @@ let registry_defaults = [ "matita.system", "false"; "matita.verbosity", "1"; "matita.bench", "false"; - "matita.paste_unicode_as_tex", "false" + "matita.paste_unicode_as_tex", "false"; + "matita.noinnertypes", "false"; + "matita.do_heavy_checks", "true"; (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is * intuitively verbose *) ] let set_registry_values = - List.iter (fun key, value -> Helm_registry.set ~key ~value) + List.iter + (fun key, value -> + if not (Helm_registry.has key) then Helm_registry.set ~key ~value) let fill_registry init_status = if not (already_configured [ Registry ] init_status) then begin @@ -68,7 +70,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; @@ -115,7 +116,7 @@ let initialize_makelib init_status = init_status let initialize_environment init_status = - wants [ConfigurationFile] init_status; + wants [CmdLine] init_status; if not (already_configured [Getter;Environment] init_status) then begin Http_getter.init (); @@ -138,44 +139,44 @@ 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", - sprintf "Matita's prover v%s + 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) @@ -212,7 +213,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 @@ -226,6 +228,7 @@ 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 + wants [Registry] init_status; let includes = ref [] in let default_includes = [ "."; @@ -240,9 +243,13 @@ let parse_cmdline init_status = let reduce_verbosity () = Helm_registry.set_int "matita.verbosity" (Helm_registry.get_int "matita.verbosity" - 1) in + let print_version () = + Printf.printf "%s\n" BuildTimeConf.version;exit 0 in let increase_verbosity () = Helm_registry.set_int "matita.verbosity" (Helm_registry.get_int "matita.verbosity" + 1) in + let no_innertypes () = + Helm_registry.set_bool "matita.noinnertypes" true in let arg_spec = let std_arg_spec = [ "-I", Arg.String (add_l includes), @@ -258,6 +265,8 @@ let parse_cmdline init_status = "-noprofile", Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), "Turns off profiling printings"; + "-noinnertypes", Arg.Unit no_innertypes, + "Turns off inner types generation while publishing"; "-profile-only", Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), "Activates only profiler with label matching the provided regex"; @@ -273,6 +282,7 @@ let parse_cmdline init_status = ("Act on the system library instead of the user one" ^ "\n WARNING: not for the casual user"); "-v", Arg.Unit increase_verbosity, "Increase verbosity"; + "--version", Arg.Unit print_version, "Prints version"; ] in let debug_arg_spec = if BuildTimeConf.debug then @@ -280,6 +290,9 @@ 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 @@ -309,11 +322,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 @@ -321,14 +339,11 @@ 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 -;; +let initialize_environment () = + status := initialize_environment !status -Inversion_principle.init () +let _ = + Inversion_principle.init ()