X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=660be6c10b76856a78fef83800945ccbf16ee03e;hb=3ea21b6d721c759876aa53385b421cb1412e11f5;hp=df29edc3b7421049ec63eb5a4616560fbfcb07fd;hpb=a458a3e72fd374b106481a7e98f4000369c6ae61;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index df29edc3b..660be6c10 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -222,3 +222,32 @@ let alias_diff ~from status =
          acc)
     status.aliases Map.empty
 
+let remove uri =
+  let derived_uris_of_uri uri =
+    UriManager.innertypesuri_of_uri uri ::
+    UriManager.annuri_of_uri uri ::
+    (match UriManager.bodyuri_of_uri uri with
+    | None -> []
+    | Some u -> [u])
+  in
+  let to_remove =
+    uri :: 
+    (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @
+    derived_uris_of_uri uri   
+  in   
+  List.iter 
+    (fun uri -> 
+      (try
+        let path = 
+          let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in
+          assert (String.sub path 0 7 = "file://");
+          String.sub path 7 (String.length path - 7)
+        in
+        remove_object_from_disk uri path; 
+      with
+        Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri);
+      remove_coercion uri; 
+      ignore(MatitaDb.remove_uri uri))
+  to_remove
+  
+