From 811ed22e8dcb12d8c88e2c320bbc2221bdff30ab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 Oct 2017 15:09:21 +0200 Subject: Implementing a generic mechanism for locating named objects from Coq side. --- printing/prettyp.mli | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'printing/prettyp.mli') 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; -- cgit v1.2.3