X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=fc952ba4f02662577ea0d22f3f3a2caf5a7d893c;hb=1b8e1a82cc00b265f2d36b2ff3d363f61cb679ea;hp=4005aeb11b4a6a77dc446b67c709fb33da297632;hpb=ebc030d495380b9f9c3b1f2a8673d84555744dd1;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4005aeb11..fc952ba4f 100644
--- 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;