* http://helm.cs.unibo.it/
*)
+open Printf
+
type thingsToInitilaize =
ConfigurationFile | Db | Environment | Getter | Notation |
- Paramodulation | Makelib
+ Paramodulation | Makelib | CmdLine
exception FailedToInitialize of thingsToInitilaize
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 ();
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 =
+ [ "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 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)");
+ ] 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;
+Helm_registry.save_to "./foo.conf.xml";
+ CmdLine :: init_status
+ end else
+ init_status
+
+let die_usage () =
+ print_endline (usage ());
+ exit 1
+
let initialize_all () =
status :=
initialize_notation
(initialize_db
(initialize_paramodulation
(initialize_makelib
- (load_configuration !status)))))
+ (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
+