X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=609a014d0f3b573ac9b152ca9816fb880668911a;hb=2bd3b029f7f67d9c616b7756278573cc9e96510c;hp=1645184264b6e446f35b196da1aae353daa7b1df;hpb=9f49495f5f1e54ccacb8142043cba65ca55b7125;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 164518426..609a014d0 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -32,7 +32,14 @@ open GrafiteTypes
 
 (** {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} *)
@@ -139,8 +146,11 @@ let _ =
       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 _ ->
@@ -252,6 +262,18 @@ let _ =
   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: *)