+
+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 [ BuildTimeConf.stdlib_dir ] 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
+