]> matita.cs.unibo.it Git - helm.git/commitdiff
- matitaclean greatly improved but ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 18 Aug 2011 20:11:59 +0000 (20:11 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 18 Aug 2011 20:11:59 +0000 (20:11 +0000)
...  LibraryClean.clean_baseuris is not implemented yet :D

matita/matita/matitaclean.ml

index d04e9fba9fab806ac32f0bc337f8967d31ca6a75..883aa3976196c8d55278a4e82f4d8cbcecb9aece 100644 (file)
@@ -25,9 +25,7 @@
 
 (* $Id$ *)
 
-open Printf
-
-module TA = GrafiteAst
+module L = Librarian
 
 let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ]
 
@@ -52,7 +50,6 @@ let ask_confirmation _ =
       flush stdout;
       exit 1
     end
-;;
 
 let clean_all () =
   if Helm_registry.get_bool "matita.system" then
@@ -72,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 
@@ -80,42 +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 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
-    | [ "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 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 = 
-         (*MATITA 1.0, CSC: verify that suri is a reasonable uri *)
          (*try*)
            NUri.baseuri_of_uri (NUri.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
+           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 *)
-       in
-        uri::uris_to_remove) [] files
-  in
-   LibraryClean.clean_baseuris uris_to_remove
+*)
+
+let main () =
+  let _ = MatitaInit.initialize_all () in
+  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
+  match Helm_registry.get_list Helm_registry.string "matita.args" with
+    | [ "all" ] -> clean_all (); exit 0
+    | []        -> 
+        let items = get_all_scripts () in
+       remove_all_items items
+    | items     ->     
+       remove_all_items items