Module Nametab.XRefs

NAMETAB extended with warnings associated to some of the elements.

include NAMETAB with type elt = Globnames.extended_global_reference

The type of the elements of the name table (eg ModPath.t)

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).

  • raises Not_found

    for unknown objects.

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 pr : elt -> Pp.t

Print using shortest_qualid and empty avoid set.

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.

When visibility is Until, wdata may be Some _ in which case the warning data is associated to the element.

Return the warning data associated to the element.

Emit the given warning data for the given element (if the warning is not disabled).

val locate : ?nowarn:bool -> Libnames.qualid -> elt

Unless nowarn:false is given, if the found element is associated to a warning, that warning is emitted.