open MatitaGtkMisc
open MatitaTypes
-open MatitaMisc
(** {2 Initialization} *)
addDebugItem "getter: getalluris" (fun _ ->
List.iter prerr_endline (Http_getter.getalluris ()));
addDebugItem "dump script status" script#dump;
+ addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
+ Helm_registry.save_to "./foo.conf.xml");
addDebugItem "dump metasenv"
(fun _ ->
if script#onGoingProof () then
CicNotationParser.print_l2_pattern;
addDebugItem "dump moo to stderr" (fun _ ->
let status = (MatitaScript.instance ())#status in
+ let moo, metadata = status.moo_content_rev in
List.iter (fun cmd -> prerr_endline
- (GrafiteAstPp.pp_command cmd)) (List.rev status.moo_content_rev));
+ (GrafiteAstPp.pp_command cmd)) (List.rev moo);
+ List.iter (fun m -> prerr_endline
+ (GrafiteAstPp.pp_metadata m)) metadata);
addDebugItem "rotate light bulbs"
(fun _ ->
let nb = gui#main#hintNotebook in
(** {2 Command line parsing} *)
-let debug = ref false
-let args = ref []
-let add_arg arg = args := arg :: !args
-
-let arg_spec =
- let std_arg_spec = [] in
- let debug_arg_spec =
- if BuildTimeConf.debug then
- [ "-debug", Arg.Set debug,
- "Do not catch top-level exception (useful for backtrace inspection)"; ]
- else []
- in
- std_arg_spec @ debug_arg_spec
-
-let usage () =
- let heading = sprintf "Matita v%s\nUsage: " BuildTimeConf.version in
- if Helm_registry.get "matita.mode" = "cicbrowser" then
- heading ^ "cicbrowser [ URL | Whelp query ]\nOptions:"
- else
- heading ^ "matita [ FILE ]"
-
let set_matita_mode () =
let matita_mode =
if Filename.basename Sys.argv.(0) = "cicbrowser"
let _ =
set_matita_mode ();
- Arg.parse arg_spec add_arg (usage ());
- Helm_registry.set_bool "matita.catch_top_level_exn" (not !debug);
at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
Sys.catch_break true;
+ let args = Helm_registry.get_list Helm_registry.string "matita.args" in
if Helm_registry.get "matita.mode" = "cicbrowser" then (* cicbrowser *)
let browser = MatitaMathView.cicBrowser () in
- let uri = match !args with [] -> "cic:/" | _ -> String.concat " " !args in
+ let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in
browser#loadInput uri
else begin (* matita *)
- (try gui#loadScript (List.hd !args) with Failure _ -> ());
+ (try gui#loadScript (List.hd args) with Failure _ -> ());
gui#main#mainWin#show ();
end;
try