open Printf
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Notation |
- Paramodulation | Makelib | CmdLine
+ ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
exception FailedToInitialize of thingsToInitilaize
let already_configured s l =
List.for_all (fun item -> List.exists (fun x -> x = item) l) s
+let tilde_expand_key k =
+ try
+ Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+ with Helm_registry.Key_not_found _ -> ()
+
let load_configuration init_status =
if not (already_configured [ConfigurationFile] init_status) then
begin
Helm_registry.load_from BuildTimeConf.matita_conf;
+ 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;
+ tilde_expand_key "matita.basedir";
+ tilde_expand_key "user.home";
ConfigurationFile::init_status
end
else
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
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";
+ [
+ "db.nodb", "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 =
"-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
("Avoid using external database connection "
^ "(WARNING: disable many features)");
+ "-noprofile",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
+ "Turns off profiling printings";
] in
let debug_arg_spec =
if BuildTimeConf.debug then
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
let initialize_all () =
status :=
- initialize_notation
+ List.fold_left (fun s f -> f s) !status
+ [ parse_cmdline; load_configuration; initialize_makelib;
+ initialize_db; initialize_environment; initialize_notation ]
+(* 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