* http://helm.cs.unibo.it/
*)
+open Printf
+
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Notation |
- Paramodulation | Makelib
+ 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
init_status
let initialize_db init_status =
- wants [ConfigurationFile] init_status;
- if not (already_configured [Db] init_status) then
+ 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 ();
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
init_status
let status = ref []
-
+
+let usages = Hashtbl.create 11
+let _ =
+ List.iter
+ (fun (name, s) -> Hashtbl.replace usages name s)
+ [ "matitac",
+ sprintf "MatitaC v%s
+Usage: matitac [ OPTION ... ] FILE
+Options:"
+ BuildTimeConf.version;
+ "matita",
+ sprintf "Matita v%s
+Usage: matita [ OPTION ... ] [ FILE ... ]
+Options:"
+ BuildTimeConf.version;
+ "cicbrowser",
+ sprintf
+ "CIC Browser v%s
+Usage: cicbrowser [ URL | WHELP QUERY ]
+Options:"
+ BuildTimeConf.version;
+ "matitadep",
+ sprintf "MatitaDep v%s
+Usage: matitadep [ OPTION ... ] FILE ...
+Options:"
+ BuildTimeConf.version;
+ "matitaclean",
+ sprintf "MatitaClean v%s
+Usage: matitaclean all
+ matitaclean [ (FILE | URI) ... ]
+Options:"
+ BuildTimeConf.version;
+ ]
+let default_usage =
+ sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
+
+let usage () =
+ let basename = Filename.basename Sys.argv.(0) in
+ let usage_key =
+ try Filename.chop_extension basename with Invalid_argument _ -> basename
+ in
+ try Hashtbl.find usages usage_key with Not_found -> default_usage
+
+let registry_defaults =
+ [
+ "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 =
+ 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 args = ref [] in
+ let add_l l = fun s -> l := s :: !l in
+ let arg_spec =
+ let std_arg_spec = [
+ "-I", Arg.String (add_l includes),
+ ("<path> Adds path to the list of searched paths for the "
+ ^ "include command");
+ "-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)");
+ "-noprofile",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
+ "Turns off profiling printings";
+ ] in
+ let debug_arg_spec =
+ if BuildTimeConf.debug then
+ [ "-debug",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
+ ("Do not catch top-level exception "
+ ^ "(useful for backtrace inspection)");
+ ]
+ else []
+ in
+ std_arg_spec @ debug_arg_spec
+ in
+ 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
+
+let die_usage () =
+ print_endline (usage ());
+ exit 1
+
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 !status)))))
+ (initialize_makelib
+ (load_configuration
+ (parse_cmdline !status))))) *)
-let load_config_only () =
+let load_configuration_file () =
status := load_configuration !status
let initialize_notation () =
status := initialize_notation (load_configuration !status)
-
+
+let parse_cmdline () =
+ status := parse_cmdline !status
+
projects / helm.git / blobdiff