diff options
| -rw-r--r-- | intf/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 65 | ||||
| -rw-r--r-- | printing/prettyp.mli | 26 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
6 files changed, 84 insertions, 16 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 03e8ea43d..4a471d4a2 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -91,7 +91,7 @@ type locatable = | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference - | LocateTactic of reference + | LocateOther of string * reference | LocateFile of string type showable = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 819d236cd..3e0b85b54 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1020,8 +1020,7 @@ GEXTEND Gram | 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 - | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] + | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: [ [ n = integer -> IntValue (Some n) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 10dd42ea9..a1cdfdbaa 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1156,7 +1156,7 @@ open Decl_kinds | LocateFile f -> keyword "File" ++ spc() ++ qs f | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid - | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid + | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid in return (keyword "Locate" ++ spc() ++ pr_locate loc) | VernacRegister (id, RegisterInline) -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b2e7fe447..2077526db 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -304,13 +304,33 @@ let print_inductive_argument_scopes = (*********************) (* "Locate" commands *) +type 'a locatable_info = { + locate : qualid -> 'a option; + locate_all : qualid -> 'a list; + shortest_qualid : 'a -> qualid; + name : 'a -> Pp.t; + print : 'a -> Pp.t; + about : 'a -> Pp.t; +} + +type locatable = Locatable : 'a locatable_info -> locatable + type logical_name = | Term of global_reference | Dir of global_dir_reference | Syntactic of kernel_name | ModuleType of module_path + | Other : 'a * 'a locatable_info -> logical_name | Undefined of qualid +(** Generic table for objects that are accessible through a name. *) +let locatable_map : locatable String.Map.t ref = ref String.Map.empty + +let register_locatable name f = + locatable_map := String.Map.add name (Locatable f) !locatable_map + +exception ObjFound of logical_name + let locate_any_name ref = let (loc,qid) = qualid_of_reference ref in try Term (Nametab.locate qid) @@ -320,7 +340,13 @@ let locate_any_name ref = try Dir (Nametab.locate_dir qid) with Not_found -> try ModuleType (Nametab.locate_modtype qid) - with Not_found -> Undefined qid + with Not_found -> + let iter _ (Locatable info) = match info.locate qid with + | None -> () + | Some ans -> raise (ObjFound (Other (ans, info))) + in + try String.Map.iter iter !locatable_map; Undefined qid + with ObjFound obj -> obj let pr_located_qualid = function | Term ref -> @@ -343,6 +369,7 @@ let pr_located_qualid = function str s ++ spc () ++ pr_dirpath dir | ModuleType mp -> str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) + | Other (obj, info) -> info.name obj | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." @@ -401,12 +428,30 @@ let locate_modtype qid = in modtypes @ List.map_filter map all +let locate_other s qid = + let Locatable info = String.Map.find s !locatable_map in + let ans = info.locate_all qid in + let map obj = (Other (obj, info), info.shortest_qualid obj) in + List.map map ans + +type locatable_kind = +| LocTerm +| LocModule +| LocOther of string +| LocAny + let print_located_qualid name flags ref = let (loc,qid) = qualid_of_reference ref in - let 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 + let located = match flags with + | LocTerm -> locate_term qid + | LocModule -> locate_modtype qid @ locate_module qid + | LocOther s -> locate_other s qid + | LocAny -> + locate_term qid @ + locate_modtype qid @ + locate_module qid @ + String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map [] + in match located with | [] -> let (dir,id) = repr_qualid qid in @@ -424,10 +469,10 @@ let print_located_qualid name flags ref = else mt ()) ++ display_alias o)) l -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_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref -let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref +let print_located_term ref = print_located_qualid "term" LocTerm ref +let print_located_other s ref = print_located_qualid s (LocOther s) ref +let print_located_module ref = print_located_qualid "module" LocModule ref +let print_located_qualid ref = print_located_qualid "object" LocAny ref (******************************************) (**** Printing declarations and judgments *) @@ -757,6 +802,7 @@ let print_any_name = function | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp + | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in @@ -815,6 +861,7 @@ let print_about_any ?loc k = hov 0 (str "Expands to: " ++ pr_located_qualid k)) | Dir _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k) + | Other (obj, info) -> hov 0 (info.about obj) let print_about = function | ByNotation (loc,(ntn,sc)) -> diff --git a/printing/prettyp.mli b/printing/prettyp.mli index f4277b6c5..dbd101159 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -50,12 +50,34 @@ val print_all_instances : unit -> Pp.t val inspect : int -> Pp.t -(** Locate *) +(** {5 Locate} *) + +type 'a locatable_info = { + locate : qualid -> 'a option; + (** Locate the most precise object with the provided name if any. *) + locate_all : qualid -> 'a list; + (** Locate all objects whose name is a suffix of the provided name *) + shortest_qualid : 'a -> qualid; + (** Return the shortest name in the current context *) + name : 'a -> Pp.t; + (** Data as printed by the Locate command *) + print : 'a -> Pp.t; + (** Data as printed by the Print command *) + about : 'a -> Pp.t; + (** Data as printed by the About command *) +} +(** Generic data structure representing locatable objects. *) + +val register_locatable : string -> 'a locatable_info -> unit +(** Define a new type of locatable objects that can be reached via the + corresponding generic vernacular commands. The string should be a unique + name describing the kind of objects considered and that is added as a + grammar command prefix for vernacular commands Locate. *) val print_located_qualid : reference -> Pp.t val print_located_term : reference -> Pp.t -val print_located_tactic : reference -> Pp.t val print_located_module : reference -> Pp.t +val print_located_other : string -> reference -> Pp.t type object_pr = { print_inductive : mutual_inductive -> Pp.t; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 83296cf58..203d913db 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) - | LocateTactic qid -> msg_notice (print_located_tactic qid) + | LocateOther (s, qid) -> msg_notice (print_located_other s qid) | LocateFile f -> msg_notice (locate_file f) let vernac_register id r = |