X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitaclean.ml;h=cf8bf42f4467f0628e93dad1d2d9b625a87112ec;hb=a957099550619f87a58be467b9b11f2ad6501378;hp=151bb011577416a31bf7b41a81d2bdc6a2acba70;hpb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;p=helm.git

diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml
index 151bb0115..cf8bf42f4 100644
--- a/matita/matitaclean.ml
+++ b/matita/matitaclean.ml
@@ -32,10 +32,36 @@ module TA = GrafiteAst
 
 let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ]
 
+let ask_confirmation _ =
+  print_string "
+  You are trying to delete the whole standard library.
+  Since this may be a dangerous operation, you are asked to type
+    
+    yes, I'm sure
+    
+  verbatim and press enter.\n\n> ";
+  flush stdout;
+  let str = input_line stdin in
+  if str = "yes, I'm sure" then 
+    begin
+      print_string "deletion in progess...\n";
+      flush stdout
+    end
+  else 
+    begin
+      print_string "deletion cancelled.\n";
+      flush stdout;
+      exit 1
+    end
+;;
+
 let main () =
   let _ = MatitaInit.initialize_all () in
+  if Helm_registry.get_bool "matita.bench" then MatitaMisc.shutup ();
   match Helm_registry.get_list Helm_registry.string "matita.args" with
   | [ "all" ] ->
+      if Helm_registry.get_bool "matita.system" then
+        ask_confirmation ();
       LibraryDb.clean_owner_environment ();
       let prefixes = 
         HExtlib.filter_map 
@@ -69,7 +95,7 @@ let main () =
             try
               UM.buri_of_uri (UM.uri_of_string suri)
             with UM.IllFormedUri _ ->
-              let u =
+              let u,_ =
                DependenciesParser.baseuri_of_script ~include_paths:[] suri in
               if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
                 HLog.error (sprintf "File %s defines a bad baseuri: %s"