completed support for "-nodb", now also matitaclean and its library work with that...

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 754197bb77fdc59fd6f21564ec6cb75609552f76..cbf305261eb3fbdcba374c23e4b8721192fec41d 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -47,6 +47,18 @@ let alias_diff =
  fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
+ let commands_of_aliases =
+   List.map
+    (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias))
+ in
+ let deps_of_aliases =
+   HExtlib.filter_map
+    (function
+    | GrafiteAst.Ident_alias (_, suri) ->
+        let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+        Some (GrafiteAst.Dependency buri)
+    | _ -> None)
+ in
  let aliases =
   List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
    status.aliases new_aliases in
@@ -59,9 +71,12 @@ let set_proof_aliases status new_aliases =
  if new_aliases = [] then
    new_status
  else
-   add_moo_content
-    (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases)
-    new_status
+   let aliases = 
+     DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+   in
+   let status = add_moo_content (commands_of_aliases aliases) new_status in
+   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate automatic aliases **)