diff options
| -rw-r--r-- | library/nametab.ml | 20 | ||||
| -rw-r--r-- | library/nametab.mli | 7 |
2 files changed, 25 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 06ace373c3..029d850504 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -74,6 +74,8 @@ 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 + (** Matches a prefix of [qualid], useful for completion *) + val match_prefixes : qualid -> t -> elt list end module Make (U : UserName) (E : EqualityType) : NAMETREE @@ -259,9 +261,19 @@ let find_prefixes qid tab = search_prefixes (Id.Map.find id tab) (DirPath.repr dir) with Not_found -> [] -end - +let match_prefixes = + let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in + fun qid tab -> + try + let (dir,id) = repr_qualid qid in + let id_prefix = cprefix Id.(to_string id) in + let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in + let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in + (* Coq's flatten is "magical", so this is not so bad perf-wise *) + CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches []) + with Not_found -> [] +end (* Global name tables *************************************************) @@ -447,6 +459,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab +(* Completion *) +let completion_canditates qualid = + ExtRefTab.match_prefixes qualid !the_ccitab + (* Derived functions *) let locate_constant qid = 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) : |