method disambiguate_db: db
end
-class virtual status =
+class virtual status uid =
object (self)
- inherit Interpretations.status
+ 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)
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)
;;
let disambiguate_nterm status expty context metasenv subst thing
-=
+=
let newast, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
~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
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
;;
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
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