* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
+ ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
exception FailedToInitialize of thingsToInitilaize
if not (already_configured [ Db ] init_status) then
begin
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
- MatitaDb.create_owner_environment ();
+ LibraryDb.create_owner_environment ();
Db::init_status
end
else
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
"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
status :=
List.fold_left (fun s f -> f s) !status
[ parse_cmdline; load_configuration; initialize_makelib;
- initialize_db; initialize_environment; initialize_notation ]
+ initialize_db; initialize_environment ]
(* initialize_notation
(initialize_environment
(initialize_db
let load_configuration_file () =
status := load_configuration !status
-let initialize_notation () =
- status := initialize_notation (load_configuration !status)
-
let parse_cmdline () =
status := parse_cmdline !status