(** {2 Initialization} *)
-let _ = MatitaInit.initialize_all ()
+let _ =
+ MatitaInit.add_cmdline_spec
+ ["-tptppath",Arg.String
+ (fun s -> Helm_registry.set_string "matita.tptppath" s),
+ "Where to find the Axioms/ and Problems/ directory"];
+ MatitaInit.initialize_all ()
+;;
+
(* let _ = Saturation.init () (* ALB to link paramodulation *) *)
(** {2 GUI callbacks} *)
let moo = grafite_status.moo_content_rev in
List.iter
(fun cmd ->
- prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false)
- cmd))
+ prerr_endline
+ (GrafiteAstPp.pp_command
+ ~term_pp:(fun _ -> assert false)
+ ~obj_pp:(fun _ -> assert false)
+ cmd))
(List.rev moo));
addDebugItem "print metasenv goals and stack to stderr"
(fun _ ->
end;
try
GtkThread.main ()
- with Sys.Break -> ()
+ with Sys.Break ->
+ Sys.set_signal Sys.sigint
+ (Sys.Signal_handle
+ (fun _ ->
+ prerr_endline "Still cleaning the library: don't be impatient!"));
+ prerr_endline "Matita is cleaning up. Please wait.";
+ try
+ let baseuri =
+ GrafiteTypes.get_string_option
+ (MatitaScript.current ())#grafite_status "baseuri"
+ in
+ LibraryClean.clean_baseuris [baseuri]
+ with GrafiteTypes.Option_error _ -> ()
(* vim:set foldmethod=marker: *)