Less feedback during removal of objects.

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4005aeb11b4a6a77dc446b67c709fb33da297632..fc952ba4f02662577ea0d22f3f3a2caf5a7d893c 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -286,6 +286,8 @@ let time_travel ~present ~past =
       List.iter MatitaLog.debug l2
       *)
     
+let last_baseuri = ref ""
+
 let remove ~verbose uri =
   let derived_uris_of_uri uri =
     UriManager.innertypesuri_of_uri uri ::
@@ -302,8 +304,14 @@ let remove ~verbose uri =
   List.iter 
     (fun uri -> 
       (try
+        (* WARNING: non reentrant debugging code *)
         if verbose then
-         MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
+         let baseuri = UriManager.buri_of_uri uri in
+          if !last_baseuri <> baseuri then
+           begin
+            MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
+            last_baseuri := baseuri
+           end;
         MatitaMisc.safe_remove (Http_getter.resolve' uri)
       with Http_getter_types.Key_not_found _ -> ());
       remove_coercion uri;