This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 4b1bdfcc872f32cb9bcf22f4fd6b8899d6148f5c..3bede228d7bafec765e2df7cac49c6527c01535e 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -54,6 +54,7 @@ class type g_status =
 class virtual status uid =
  object (self)
   inherit Interpretations.status uid
+  inherit NCicLibrary.status uid
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
@@ -158,13 +159,13 @@ let mk_implicit b =
       GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 ;;
 
-let nlookup_in_library 
+let nlookup_in_library status
   interactive_user_uri_choice input_or_locate_uri item 
 =
   match item with
   | DisambiguateTypes.Id id -> 
      (try
-       let references = NCicLibrary.resolve id in
+       let references = NCicLibrary.resolve status id in
         List.map
          (fun u -> 
            GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
@@ -295,7 +296,7 @@ let diff_obj loc o1 o2 = match o1,o2 with
 ;;
 
 let disambiguate_nterm status expty context metasenv subst thing
-=
+= 
   let newast, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
@@ -303,7 +304,7 @@ let disambiguate_nterm status expty context metasenv subst thing
         ~aliases:status#disambiguate_db.interpr
         ~expty 
         ~universe:(status#disambiguate_db.multi_aliases)
-        ~lookup_in_library:nlookup_in_library
+        ~lookup_in_library:(nlookup_in_library status)
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
@@ -311,7 +312,7 @@ let disambiguate_nterm status expty context metasenv subst thing
   in
   let _,_,thing' = thing in
   let diff = diff_term Stdpp.dummy_loc thing' newast in
-  let status = add_to_interpr status diff
+  let status = add_to_interpr status diff 
   in
    metasenv, subst, status, cic
 ;;
@@ -382,7 +383,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
    singleton "third"
     (NCicDisambiguate.disambiguate_obj
       status
-      ~lookup_in_library:nlookup_in_library
+      ~lookup_in_library:(nlookup_in_library status)
       ~description_of_alias:GrafiteAst.description_of_alias
       ~mk_choice:(ncic_mk_choice status)
       ~mk_implicit ~fix_instance ~uri
@@ -435,7 +436,7 @@ let aliases_for_objs status refs =
  List.concat
   (List.map
     (fun nref ->
-      let references = NCicLibrary.aliases_of nref in
+      let references = NCicLibrary.aliases_of status nref in
        List.map
         (fun u ->
           let name = NCicPp.r2s status true u in