From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jul 2006 10:04:02 +0000 (+0000)
Subject: Ctr-C now cleans up (with a nice warning :-)
X-Git-Tag: 0.4.95@7852~1183
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=872dbd15c8f6d10c2b9b46ad6f995bf494c23e65;p=helm.git

Ctr-C now cleans up (with a nice warning :-)
---

diff --git a/matita/matita.ml b/matita/matita.ml
index 164518426..a70063f5f 100644
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -252,6 +252,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: *)