diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 18 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 2 |
2 files changed, 20 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 114410fed..3d1e3e054 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -366,6 +366,24 @@ module Make in str "<" ++ name ++ str ">" ++ args + + let pr_alias_key key = + try + let prods = (KNmap.find key !prnotation_tab).pptac_prods in + (* First printing strategy: only the head symbol *) + match prods with + | TacTerm s :: prods -> str s + | _ -> + (* Second printing strategy; if ever Tactic Notation is eventually *) + (* accepting notations not starting with an identifier *) + let rec pr = function + | [] -> [] + | TacTerm s :: prods -> s :: pr prods + | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in + str (String.concat " " (pr prods)) + with Not_found -> + KerName.print key + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 4ef2ea918..f02785a55 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -45,6 +45,8 @@ module type Pp = sig val pr_extend : (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_alias : (Val.t -> std_ppcmds) -> int -> Names.KerName.t -> Val.t list -> std_ppcmds |