Unifying locate code, also making it more powerful: it is now able to find

any prefix of the given qualid.

5 files changed, 29 insertions, 18 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index edceacaa8..3bd4e03ab 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -431,6 +431,8 @@ let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab
 
 let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
 
+let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
+
 (* Derived functions *)
 
 let locate_constant qid =
@@ -490,6 +492,9 @@ let dirpath_of_module mp =
 let path_of_tactic kn =
   KNmap.find kn !the_tacticrevtab
 
+let path_of_modtype mp =
+  MPmap.find mp !the_modtyperevtab
+
 (* Shortest qualid functions **********************************************)
 
 let shortest_qualid_of_global ctx ref =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1289a6745..eb2cecc59 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -113,6 +113,7 @@ val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_tactic : qualid -> ltac_constant list
 val locate_extended_all_dir : qualid -> global_dir_reference list
+val locate_extended_all_modtype : qualid -> module_path list
 
 (** Mapping a full path to a global reference *)
 
@@ -143,6 +144,7 @@ val full_name_module : qualid -> DirPath.t
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
 val dirpath_of_module : module_path -> DirPath.t
+val path_of_modtype : module_path -> full_path
 val path_of_tactic : ltac_constant -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index c5840e20b..67b3df35e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -262,7 +262,7 @@ type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
   | Syntactic of kernel_name
-  | ModuleType of qualid * module_path
+  | ModuleType of module_path
   | Tactic of Nametab.ltac_constant
   | Undefined of qualid
 
@@ -274,7 +274,7 @@ let locate_any_name ref =
   with Not_found ->
   try Dir (Nametab.locate_dir qid)
   with Not_found ->
-  try ModuleType (qid, Nametab.locate_modtype qid)
+  try ModuleType (Nametab.locate_modtype qid)
   with Not_found -> Undefined qid
 
 let pr_located_qualid = function
@@ -296,8 +296,8 @@ let pr_located_qualid = function
 	| DirClosedSection dir -> "Closed Section", dir
       in
       str s ++ spc () ++ pr_dirpath dir
-  | ModuleType (qid,_) ->
-      str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid)
+  | ModuleType mp ->
+      str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
   | Tactic kn ->
       str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn)
   | Undefined qid ->
@@ -350,10 +350,23 @@ let locate_module qid =
   in
   List.map_filter map all
 
+let locate_modtype qid =
+  let all = Nametab.locate_extended_all_modtype qid in
+  let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in
+  let modtypes = List.map map all in
+  (** Don't forget the opened module types: they are not part of the same name tab. *)
+  let all = Nametab.locate_extended_all_dir qid in
+  let map dir = match dir with
+  | DirOpenModtype _ -> Some (Dir dir, qid)
+  | _ -> None
+  in
+  modtypes @ List.map_filter map all
+
 let print_located_qualid name flags ref =
   let (loc,qid) = qualid_of_reference ref in
   let located = [] in
   let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in
+  let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in
   let located = if List.mem `MODULE flags then locate_module qid @ located else located in
   let located = if List.mem `TERM flags then locate_term qid @ located else located in
   match located with
@@ -375,7 +388,8 @@ let print_located_qualid name flags ref =
 
 let print_located_term ref = print_located_qualid "term" [`TERM] ref
 let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref
-let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE] ref
+let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref
+let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref
 
 (******************************************)
 (**** Printing declarations and judgments *)
@@ -662,7 +676,7 @@ let print_any_name = function
   | Syntactic kn -> print_syntactic_def kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
-  | ModuleType (_,kn) -> print_modtype kn
+  | ModuleType mp -> print_modtype mp
   | Tactic kn -> mt () (** TODO *)
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index de34131fe..595637745 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -57,6 +57,7 @@ val inspect : int -> std_ppcmds
 val print_located_qualid : reference -> std_ppcmds
 val print_located_term : reference -> std_ppcmds
 val print_located_tactic : reference -> std_ppcmds
+val print_located_module : reference -> std_ppcmds
 
 type object_pr = {
   print_inductive           : mutual_inductive -> std_ppcmds;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4141f9f56..4106d29df 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -397,17 +397,6 @@ let print_located_library r =
     | Library.LibUnmappedDir -> err_unmapped_library loc qid
     | Library.LibNotFound -> err_notfound_library loc qid
 
-let print_located_module r =
-  let (loc,qid) = qualid_of_reference r in
-  try
-    let dir = Nametab.full_name_module qid in
-    msg_notice (str "Module " ++ pr_dirpath dir)
-  with Not_found ->
-    if DirPath.is_empty (fst (repr_qualid qid)) then
-      msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid)
-    else
-      msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid)
-
 let smart_global r =
   let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr;
@@ -1540,7 +1529,7 @@ let vernac_locate = function
         (Notation.locate_notation
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
-  | LocateModule qid -> print_located_module qid
+  | LocateModule qid -> msg_notice (print_located_module qid)
   | LocateTactic qid -> msg_notice (print_located_tactic qid)
   | LocateFile f -> msg_notice (locate_file f)