aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli1
-rw-r--r--library/nametab.ml2
-rw-r--r--library/nametab.mli1
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--printing/ppvernac.ml3
-rw-r--r--printing/prettyp.ml64
-rw-r--r--printing/prettyp.mli2
-rw-r--r--toplevel/vernacentries.ml6
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 01:47:16 +0000