* 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
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 =
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