Adding a new "Locate Term" command, distinct from the raw "Locate" command.

The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".

Fixes bug #3380.

8 files changed, 50 insertions, 32 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5aa9d51fc..f62065228 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -88,6 +88,7 @@ type searchable =
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
+  | LocateAny of reference or_by_notation
   | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
diff --git a/library/nametab.ml b/library/nametab.ml
index 4a61a9540..edceacaa8 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -429,6 +429,8 @@ let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
 let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab
 
+let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
+
 (* Derived functions *)
 
 let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index ed4200456..1289a6745 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -112,6 +112,7 @@ val global_inductive : reference -> inductive
 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
 
 (** Mapping a full path to a global reference *)
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5f49a318d..0b6fc7bf7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -908,7 +908,8 @@ GEXTEND Gram
       | qid = smart_global -> RefClass qid ] ]
   ;
   locatable:
-    [ [ qid = smart_global -> LocateTerm qid
+    [ [ qid = smart_global -> LocateAny qid
+      | IDENT "Term"; qid = smart_global -> LocateTerm qid
       | IDENT "File"; f = ne_string -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary qid
       | IDENT "Module"; qid = global -> LocateModule qid
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f088477e7..e52239ba7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -924,7 +924,8 @@ let rec pr_vernac = function
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc ->
       let pr_locate =function
-	| LocateTerm qid -> pr_smart_global qid
+        | LocateAny qid -> pr_smart_global qid
+        | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid
 	| LocateFile f -> str"File" ++ spc() ++ qs f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
 	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 42f308955..c5840e20b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -263,6 +263,7 @@ type logical_name =
   | Dir of global_dir_reference
   | Syntactic of kernel_name
   | ModuleType of qualid * module_path
+  | Tactic of Nametab.ltac_constant
   | Undefined of qualid
 
 let locate_any_name ref =
@@ -297,6 +298,8 @@ let pr_located_qualid = function
       str s ++ spc () ++ pr_dirpath dir
   | ModuleType (qid,_) ->
       str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid)
+  | Tactic kn ->
+      str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn)
   | Undefined qid ->
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -325,20 +328,41 @@ let display_alias = function
     end
   | _ -> mt ()
 
-let print_located_qualid ref =
-  let (loc,qid) = qualid_of_reference ref in
+let locate_term qid =
   let expand = function
     | TrueGlobal ref ->
-	Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref
+        Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref
     | SynDef kn ->
-	Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn in
-  match List.map expand (Nametab.locate_extended_all qid) with
+        Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn
+  in
+  List.map expand (Nametab.locate_extended_all qid)
+
+let locate_tactic qid =
+  let all = Nametab.locate_extended_all_tactic qid in
+  List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all
+
+let locate_module qid =
+  let all = Nametab.locate_extended_all_dir qid in
+  let map dir = match dir with
+  | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp)
+  | DirOpenModule _ -> Some (Dir dir, qid)
+  | _ -> None
+  in
+  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 `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
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str "No object of basename " ++ pr_id id
+	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
 	else
-	  str "No object of suffix " ++ pr_qualid qid
+	  str ("No " ^ name ^ " of suffix") ++ pr_qualid qid
     | l ->
 	prlist_with_sep fnl
 	(fun (o,oqid) ->
@@ -349,26 +373,9 @@ let print_located_qualid ref =
 	   else mt ()) ++
           display_alias o)) l
 
-let print_located_tactic r =
-  let (loc,qid) = qualid_of_reference r in
-  let all = Nametab.locate_extended_all_tactic qid in
-  let ans = List.map (fun qid -> (qid, Nametab.shortest_qualid_of_tactic qid)) all in
-  match ans with
-  | [] ->
-    str "No Ltac definition is referred to by " ++ pr_qualid qid
-  | _ ->
-    let print (obj, oqid) =
-      let path = Nametab.path_of_tactic obj in
-      let msg = str "Ltac" ++ spc () ++ pr_path path in
-      let short =
-        if not (qualid_eq oqid qid) then
-          spc() ++ str "(shorter name to refer to it in current context is "
-          ++ pr_qualid oqid ++ str")"
-        else mt ()
-      in
-      hov 2 (msg ++ short)
-    in
-    prlist_with_sep fnl print ans
+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
 
 (******************************************)
 (**** Printing declarations and judgments *)
@@ -656,6 +663,7 @@ let print_any_name = function
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
   | ModuleType (_,kn) -> print_modtype kn
+  | Tactic kn -> mt () (** TODO *)
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
@@ -710,7 +718,7 @@ let print_about_any loc k =
       v 0 (
       print_syntactic_def kn ++ fnl () ++
       hov 0 (str "Expands to: " ++ pr_located_qualid k))
-  | Dir _ | ModuleType _ | Undefined _ ->
+  | Dir _ | ModuleType _ | Tactic _ | Undefined _ ->
       hov 0 (pr_located_qualid k)
 
 let print_about = function
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index bc0ce1718..de34131fe 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -53,7 +53,9 @@ val print_all_instances : unit -> std_ppcmds
 val inspect : int -> std_ppcmds
 
 (** Locate *)
+
 val print_located_qualid : reference -> std_ppcmds
+val print_located_term : reference -> std_ppcmds
 val print_located_tactic : reference -> std_ppcmds
 
 type object_pr = {
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 737d1c523..4141f9f56 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1532,8 +1532,10 @@ let vernac_search s r =
       msg_notice (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)
 
 let vernac_locate = function
-  | LocateTerm (AN qid) -> msg_notice (print_located_qualid qid)
-  | LocateTerm (ByNotation (_,ntn,sc)) ->
+  | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
+  | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
+  | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
+  | LocateTerm (ByNotation (_, ntn, sc)) ->
       msg_notice
         (Notation.locate_notation
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)