MakeWarned.1-M
Common APIs on name tables.
val push : visibility -> Libnames.full_path -> elt -> unit
Add an element or modify its visibility. With visibility Until
, assume the element is new. With visibility Exactly
, assume the element is not new.
val remove : Libnames.full_path -> elt -> unit
Remove an element.
val shortest_qualid_gen : ?loc:Loc.t -> (Names.Id.t -> bool) -> elt -> Libnames.qualid
shortest_qualid_gen avoid v
: given an object v
with full name Mylib.A.B.x, try to find the shortest among x, B.x, A.B.x and Mylib.A.B.x that denotes the same object. If avoid
is true
on x
it is assumed to denote something else (so B.x is the shortest qualid that could be returned).
val shortest_qualid : ?loc:Loc.t -> Names.Id.Set.t -> elt -> Libnames.qualid
Like shortest_qualid_gen
but using an id set instead of a closure.
val locate : Libnames.qualid -> elt
Globalize the given user-level reference. If any warnings are associated with the produced object, print them unless nowarn:true
was given.
val locate_all : Libnames.qualid -> elt list
Locate all elements with a given suffix. If the qualid is a valid absolute name, that element is first in the list.
val completion_candidates : Libnames.qualid -> elt list
Return the elements that have the qualid as a prefix. UIs will usually compose with shortest_qualid
. Experimental APIs, please tell us if you use it.
val to_path : elt -> Libnames.full_path
Return the absolute name for the given element.
val of_path : Libnames.full_path -> elt
Return an element bound to an absolute path.
val exists : Libnames.full_path -> bool
Returns whether this absolute path is taken.