if a node has an xref use it for cut and paste, no matter if it have an href as well

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4005aeb11b4a6a77dc446b67c709fb33da297632..f2c9d6e336858c9d236524a5752c81ce1f00ce09 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -43,8 +43,8 @@ let alias_diff ~from status =
     status.aliases []
 
 let alias_diff =
- let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
  let aliases =
@@ -125,7 +125,7 @@ let paths_and_uris_of_obj uri status =
 let save_object_to_disk status uri obj ugraph univlist =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
-    MatitaMisc.mkdir dir
+    HExtlib.mkdir dir
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
@@ -139,14 +139,13 @@ let save_object_to_disk status uri obj ugraph univlist =
     paths_and_uris_of_obj uri status 
   in
   let path_scheme_of path = "file://" ^ path in
-  List.iter MatitaMisc.mkdir
-    (List.map Filename.dirname [innertypespath; xmlpath]);
+  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
   ensure_path_exists xmlpath;
   Xml.pp ~gzip:true xml (Some xmlpath);
   CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
   (* we return a list of uri,path we registered/created *)
-  (uri,xmlpath) :: (innertypesuri,innertypespath) :: 
+  (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
@@ -158,18 +157,13 @@ let save_object_to_disk status uri obj ugraph univlist =
      | _-> assert false) 
 
 let typecheck_obj =
- let profiler = CicUtil.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
+ let profiler = HExtlib.profile "add_obj.typecheck_obj" in
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
- let profiler = CicUtil.profile "add_obj.index_obj" in
+ let profiler = HExtlib.profile "add_obj.index_obj" in
   fun ~dbd ~uri ->
-   profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-
-let save_object_to_disk =
- let profiler = CicUtil.profile "add_obj.save_object_to_disk" in
-  fun status uri obj ugraph univlist ->
-   profiler.CicUtil.profile (save_object_to_disk status uri obj ugraph) univlist
+   profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
 let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
@@ -201,8 +195,8 @@ let add_obj uri obj status =
   end
 
 let add_obj =
- let profiler = CicUtil.profile "add_obj" in
-  fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
+ let profiler = HExtlib.profile "add_obj" in
+  fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
    
 module OrderedUri =
 struct
@@ -286,7 +280,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,9 +298,17 @@ 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);
-        MatitaMisc.safe_remove (Http_getter.resolve' uri)
+         let baseuri = UriManager.buri_of_uri uri in
+          if !last_baseuri <> baseuri then
+           begin
+            MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
+            last_baseuri := baseuri
+           end;
+           let file = Http_getter.resolve' uri in
+           MatitaMisc.safe_remove file;
+           MatitaMisc.rmdir_descend (Filename.dirname file)
       with Http_getter_types.Key_not_found _ -> ());
       remove_coercion uri; 
       ignore (MatitaDb.remove_uri uri);