[nametab] [api] Provide basic support for efficient completion.

We provide a function `completion_candidates id` that will return a
list of candidates global references that have id as prefix.

This should be reasonably efficient, however UI still need to call
`shortest_qualid_of_global` which is a bit heavy. How to improve this
in the future is an open question.

cc: #7164

1 files changed, 7 insertions, 0 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..1e479b200b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -118,6 +118,12 @@ val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
+(** Experimental completion support, API is _unstable_ *)
+val completion_canditates : qualid -> extended_global_reference list
+(** [completion_canditates qualid] will return the list of global
+    references that have [qualid] as a prefix. UI usually will want to
+    compose this with [shortest_qualid_of_global] *)
+
 (** Mapping a full path to a global reference *)
 
 val global_of_path : full_path -> GlobRef.t
@@ -211,6 +217,7 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+  val match_prefixes : qualid -> t -> elt list
 end
 
 module Make (U : UserName) (E : EqualityType) :