From 1b8e1a82cc00b265f2d36b2ff3d363f61cb679ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 23 Sep 2005 14:30:00 +0000 Subject: [PATCH] Less feedback during removal of objects. --- helm/matita/matitaSync.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) 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; -- 2.39.2