OPTIMIZE table every 30 deletions: it should help :-)

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index c34084d34d3f4933fa57845a7d86f586c399da0f..8b54e98d9e767c0064bfa1bf8b8bb337dce92e9f 100644 (file)
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -160,6 +160,8 @@ let rec fix uris next =
   | [] -> uris
   | l -> let uris, next = close_uri_list l in fix uris next @ uris
   
+let cleaned_no = ref 0;;
+
 let clean_baseuris ?(verbose=true) buris =
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map HGM.strip_trailing_slash buris in
@@ -172,7 +174,15 @@ let clean_baseuris ?(verbose=true) buris =
   debug_prerr "clean_baseuri will remove:";
   if debug then
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
-  List.iter (MatitaSync.remove ~verbose) l
+  List.iter (MatitaSync.remove ~verbose) l;
+  cleaned_no := !cleaned_no + List.length l;
+  if !cleaned_no > 30 then
+   List.iter
+    (function table ->
+      ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+    [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+     MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+     MetadataTypes.count_tbl()]
   
 let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []