X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=95dab03607493fb3f56e8ddccecaadefb92cf755;hb=37daa227f906a30b6d142e03f7589961476ce50d;hp=4005aeb11b4a6a77dc446b67c709fb33da297632;hpb=03be93eb7712b24fa90fcaf7b9b79df99e1f4105;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4005aeb11..95dab0360 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -286,7 +286,9 @@ let time_travel ~present ~past =
       List.iter MatitaLog.debug l2
       *)
     
-let remove ~verbose uri =
+let last_baseuri = ref ""
+
+let remove ?(verbose=false) uri =
   let derived_uris_of_uri uri =
     UriManager.innertypesuri_of_uri uri ::
     UriManager.univgraphuri_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;