X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;h=53ff6b9d60f29bdb8d775ba61811f11b174e18ff;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=84dff49e9eced28ba3de448426503fc6550f0d56;hpb=6d1af82b714e5c6a7f33534d6832598e72cb23c3;p=helm.git diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 84dff49e9..53ff6b9d6 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -23,11 +23,12 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Notation | - Paramodulation | Makelib | CmdLine + ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry exception FailedToInitialize of thingsToInitilaize @@ -41,10 +42,40 @@ let wants s l = let already_configured s l = List.for_all (fun item -> List.exists (fun x -> x = item) l) s +let conffile = ref BuildTimeConf.matita_conf + +let registry_defaults = + [ + "db.nodb", "false"; + "matita.system", "false"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.quiet", "false"; + "matita.profile", "true"; + ] + +let set_registry_values = + List.iter (fun key, value -> Helm_registry.set ~key ~value) + +let fill_registry init_status = + if not (already_configured [ Registry ] init_status) then begin + set_registry_values registry_defaults; + Registry :: init_status + end else + init_status + let load_configuration init_status = + wants [ Registry ] init_status; if not (already_configured [ConfigurationFile] init_status) then begin - Helm_registry.load_from BuildTimeConf.matita_conf; + Helm_registry.load_from !conffile; + if not (Helm_registry.has "user.name") then begin + let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in + Helm_registry.set "user.name" login + end; + if Helm_registry.get_bool "matita.system" then + Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir; ConfigurationFile::init_status end else @@ -54,23 +85,14 @@ let initialize_db init_status = wants [ ConfigurationFile; CmdLine ] init_status; if not (already_configured [ Db ] init_status) then begin - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment (); + if not (Helm_registry.get_bool "matita.system") then + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + LibraryDb.create_owner_environment (); Db::init_status end else init_status -let initialize_paramodulation init_status = - wants [] init_status; - if not (already_configured [Paramodulation] init_status) then - begin - Paramodulation.Saturation.init (); - Paramodulation::init_status - end - else - init_status - let initialize_makelib init_status = wants [ConfigurationFile] init_status; if not (already_configured [Makelib] init_status) then @@ -81,23 +103,15 @@ let initialize_makelib init_status = else init_status -let initialize_notation init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Notation] init_status) then - begin - CicNotation.load_notation BuildTimeConf.core_notation_script; - Notation::init_status - end - else - init_status - let initialize_environment init_status = wants [ConfigurationFile] init_status; if not (already_configured [Getter;Environment] init_status) then begin Http_getter.init (); CicEnvironment.set_trust (* environment trust *) - (let trust = Helm_registry.get_bool "matita.environment_trust" in + (let trust = + Helm_registry.get_opt_default Helm_registry.get_bool + ~default:true "matita.environment_trust" in fun _ -> trust); Getter::Environment::init_status end @@ -148,19 +162,9 @@ let usage () = in try Hashtbl.find usages usage_key with Not_found -> default_usage -let registry_defaults = - [ "matita.debug", "false"; - "matita.quiet", "false"; - "matita.preserve", "false"; - "db.nodb", "false"; - ] - -let set_registry_values = - List.iter (fun key, value -> Helm_registry.set ~key ~value) - let parse_cmdline init_status = if not (already_configured [CmdLine] init_status) then begin - let includes = ref [] in + let includes = ref [ BuildTimeConf.stdlib_dir ] in let args = ref [] in let add_l l = fun s -> l := s :: !l in let arg_spec = @@ -168,14 +172,24 @@ let parse_cmdline init_status = "-I", Arg.String (add_l includes), (" Adds path to the list of searched paths for the " ^ "include command"); + "-conffile", Arg.Set_string conffile, + (Printf.sprintf " Read configuration from filename (default: %s)" + BuildTimeConf.matita_conf); "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true), "Turn off verbose compilation"; "-preserve", Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), "Turns off automatic baseuri cleaning"; "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true), - ("Avoid using external database connection " - ^ "(WARNING: disable many features)"); + ("Avoid using external database connection " + ^ "(WARNING: disable many features)"); + "-system", Arg.Unit (fun () -> + Helm_registry.set_bool "matita.system" true), + ("Act on the system library instead of the user one" + ^ "(WARNING: not for the casual user)"); + "-noprofile", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), + "Turns off profiling printings"; ] in let debug_arg_spec = if BuildTimeConf.debug then @@ -191,10 +205,11 @@ let parse_cmdline init_status = let set_list ~key l = Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l) in - set_registry_values registry_defaults; Arg.parse arg_spec (add_l args) (usage ()); set_list ~key:"matita.includes" includes; set_list ~key:"matita.args" args; + HExtlib.set_profiling_printings + (fun () -> Helm_registry.get_bool "matita.profile"); CmdLine :: init_status end else init_status @@ -205,20 +220,23 @@ let die_usage () = let initialize_all () = status := - initialize_notation + List.fold_left (fun s f -> f s) !status + [ fill_registry; + parse_cmdline; load_configuration; initialize_makelib; + initialize_db; initialize_environment ] +(* initialize_notation (initialize_environment (initialize_db - (initialize_paramodulation - (initialize_makelib - (load_configuration - (parse_cmdline !status)))))) + (initialize_makelib + (load_configuration + (parse_cmdline !status))))) *) let load_configuration_file () = status := load_configuration !status -let initialize_notation () = - status := initialize_notation (load_configuration !status) - let parse_cmdline () = status := parse_cmdline !status +let fill_registry () = + status := fill_registry !status +