Fixes a bug (introduced in the previous revision) which caused the environment

[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 30bd9b83497417ef9e3737827620de485e3b0ba2..9c7ea4768ceb4152cf35839d2cda60fcfb3f90a6 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -48,18 +48,24 @@ let initial_status = {
 class type g_status =
   object
    inherit Interpretations.g_status
+   inherit NCicLibrary.g_status
    method disambiguate_db: db
   end
 
 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 >}
+  method reset_disambiguate_db () = 
+    {< disambiguate_db = { self#disambiguate_db with interpr =
+            DisambiguateTypes.InterprEnv.empty } >}
   method set_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
+      = fun o -> ((self#set_interp_status o)#set_disambiguate_db
+      o#disambiguate_db)#set_lib_status o
  end
 
 (* let eval_with_new_aliases status f =
@@ -155,13 +161,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)
@@ -292,7 +298,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
@@ -300,7 +306,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
@@ -308,7 +314,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
 ;;
@@ -379,7 +385,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
@@ -432,7 +438,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