X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=c82caf3371eecbeccbe7605bb4a08b6a4541c313;hb=HEAD;hp=f88a79971b32919e0441a31f85bf8999840376bd;hpb=004fbb54bc0a2b971f08bcf830ac8cbdafcdbe57;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index f88a79971..c82caf337 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -28,9 +28,13 @@
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
   Map.fold
-    (fun domain_item (description1,_ as codomain_item) acc ->
+    (fun domain_item codomain_item acc ->
+      let description1 = LexiconAst.description_of_alias codomain_item in
       try
-       let description2,_ = Map.find domain_item from.LexiconEngine.aliases in
+       let description2 = 
+          LexiconAst.description_of_alias 
+            (Map.find domain_item from#lstatus.LexiconEngine.aliases)
+       in
         if description1 <> description2 then
          (domain_item,codomain_item)::acc
         else
@@ -38,11 +42,8 @@ let alias_diff ~from status =
       with
        Not_found ->
          (domain_item,codomain_item)::acc)
-    status.LexiconEngine.aliases []
-
-let alias_diff =
- let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
+    status#lstatus.LexiconEngine.aliases []
+;;
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate automatic aliases **)
@@ -60,8 +61,8 @@ let extract_alias types uri =
 let build_aliases =
  List.map
   (fun (name,uri) ->
-    DisambiguateTypes.Id name,
-     (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
+    DisambiguateTypes.Id name, LexiconAst.Ident_alias (name, 
+     UriManager.string_of_uri uri))
 
 let add_aliases_for_inductive_def status types uri = 
   let aliases = build_aliases (extract_alias types uri) in
@@ -80,16 +81,32 @@ let add_aliases_for_object status uri =
   | Cic.Variable _
   | Cic.CurrentProof _ -> assert false
   
-let add_aliases_for_objs =
- List.fold_left
-  (fun status uri ->
-    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-     add_aliases_for_object status uri obj)
+let add_aliases_for_objs status =
+ function
+    `Old uris ->
+      List.fold_left
+       (fun status uri ->
+         let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+          add_aliases_for_object status uri obj) status uris
+  | `New nrefs ->
+     List.fold_left
+      (fun status nref ->
+        let references = NCicLibrary.aliases_of nref in
+        let new_env =
+         List.map
+          (fun u ->
+            let name = NCicPp.r2s true u in
+             DisambiguateTypes.Id name,
+              LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+          ) references
+        in
+         LexiconEngine.set_proof_aliases status new_env
+      ) status nrefs
  
 module OrderedId = 
 struct
   type t = CicNotation.notation_id
-  let compare = Pervasives.compare
+  let compare =  CicNotation.compare_notation_id
 end
 
 module IdSet  = Set.Make (OrderedId)
@@ -104,8 +121,10 @@ let id_list_diff l2 l1 =
 
 let time_travel ~present ~past =
   let notation_to_remove =
-    id_list_diff present.LexiconEngine.notation_ids
-     past.LexiconEngine.notation_ids
+    id_list_diff present#lstatus.LexiconEngine.notation_ids
+     past#lstatus.LexiconEngine.notation_ids
   in
    List.iter CicNotation.remove_notation notation_to_remove
 
+let push () = CicNotation.push ();;
+let pop () = CicNotation.pop ();;