X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatitaclean.ml;h=883aa3976196c8d55278a4e82f4d8cbcecb9aece;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=a3183c16110fdeb03e273b3f55caac0baa1f08f9;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/matitaclean.ml b/matita/matita/matitaclean.ml
index a3183c161..883aa3976 100644
--- a/matita/matita/matitaclean.ml
+++ b/matita/matita/matitaclean.ml
@@ -25,10 +25,7 @@
 
 (* $Id$ *)
 
-open Printf
-
-module UM = UriManager
-module TA = GrafiteAst
+module L = Librarian
 
 let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ]
 
@@ -53,12 +50,10 @@ let ask_confirmation _ =
       flush stdout;
       exit 1
     end
-;;
 
 let clean_all () =
   if Helm_registry.get_bool "matita.system" then
     ask_confirmation ();
-  LibraryDb.clean_owner_environment ();
   let prefixes = 
     HExtlib.filter_map 
       (fun s -> 
@@ -74,7 +69,7 @@ let clean_all () =
         String.concat " -o "
           (List.map (fun suf -> "-name \\*" ^ suf) clean_suffixes) in
       let clean_cmd =
-        sprintf "find %s \\( %s \\) -exec rm \\{\\} \\; 2> /dev/null"
+        Printf.sprintf "find %s \\( %s \\) -exec rm \\{\\} \\; 2> /dev/null"
           xmldir clean_pat in
       ignore (Sys.command clean_cmd);
       ignore 
@@ -82,41 +77,50 @@ let clean_all () =
         " -type d -exec rmdir -p {} \\; 2> /dev/null"))) 
     prefixes;
   ignore (Sys.command ("rm -rf " ^ Helm_registry.get "matita.basedir"))
-;;
+
+let get_all_scripts () = 
+   match L.find_roots_in_dir (Sys.getcwd ()) with
+      | [root] ->
+         let bdir = Filename.dirname root in
+         HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") bdir
+      | []     ->
+         prerr_endline "no roots found"; exit 1
+      | roots  -> 
+         let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
+         prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
+         prerr_endline ("\nEnter one of these directories and retry");
+         exit 1
+
+let remove_all_items items =
+   let map item =
+      if L.is_uri item then item else
+      let _,buri,_,_ = L.baseuri_of_script ~include_paths:[] item in
+      buri
+   in
+(*MATITA 1.0, CSC: verify that uris_to_remove are reasonable uris *)
+   let uris_to_remove = List.map map items in
+   LibraryClean.clean_baseuris ~verbose:true uris_to_remove
+
+(* FG: Old code kept for reference
+
+       let uri = 
+         (*try*)
+           NUri.baseuri_of_uri (NUri.uri_of_string suri)
+         (*with UM.IllFormedUri _ ->
+           let _,u,_,_ = L.baseuri_of_script ~include_paths:[] suri in
+           if L.is_uri u then u else begin
+             HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u);
+             exit 1
+           end *)
+*)
 
 let main () =
   let _ = MatitaInit.initialize_all () in
   if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
-  let files =
-    match Helm_registry.get_list Helm_registry.string "matita.args" with
+  match Helm_registry.get_list Helm_registry.string "matita.args" with
     | [ "all" ] -> clean_all (); exit 0
-    | [] -> 
-        (match Librarian.find_roots_in_dir (Sys.getcwd ()) with
-        | [x] -> 
-           Sys.chdir (Filename.dirname x); 
-           HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "."
-        | [] -> 
-           prerr_endline "No targets and no root found"; exit 1
-        | roots -> 
-           let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
-           prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
-           prerr_endline ("\nEnter one of these directories and retry");
-           exit 1);
-    | files -> files
-  in
-  let uris_to_remove =
-   List.fold_left
-     (fun uris_to_remove suri ->
-       let uri = 
-         try
-           UM.buri_of_uri (UM.uri_of_string suri)
-         with UM.IllFormedUri _ ->
-           let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in
-           if Librarian.is_uri u then u else begin
-             HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u);
-             exit 1
-           end 
-       in
-        uri::uris_to_remove) [] files
-  in
-   LibraryClean.clean_baseuris uris_to_remove
+    | []        -> 
+        let items = get_all_scripts () in
+	remove_all_items items
+    | items     ->     
+    	remove_all_items items