diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 30 | ||||
| -rw-r--r-- | printing/pptactic.mli | 2 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 6 |
3 files changed, 23 insertions, 15 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a669aef9a..72d2eedcc 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -34,13 +34,14 @@ type pp_tactic = { } (* ML Extensions *) -let prtac_tab = Hashtbl.create 17 +let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = + Hashtbl.create 17 (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods + Hashtbl.add prtac_tab key pt let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -414,14 +415,18 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev s l = + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = try - let tags = List.map genarg_tag l in - let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in + let pp_rules = Hashtbl.find prtac_tab s in + let pp = pp_rules.(i) in + let (lev', pl) = pp.pptac_prods in let p = pr_tacarg_using_rule pr_gen (pl,l) in if lev' > lev then surround p else p with Not_found -> - let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let name = + str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ + str "@" ++ int i + in let args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l @@ -756,7 +761,7 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds; pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; } @@ -1375,9 +1380,9 @@ module Make pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; - pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); - pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); - pr_constant = pr_and_short_name (pr_evaluable_reference_env env); + pr_pattern = pr_constr_pattern_env env Evd.empty; + pr_lpattern = pr_lconstr_pattern_env env Evd.empty; + pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; @@ -1432,6 +1437,9 @@ end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1442,7 +1450,7 @@ let () = Constrarg.wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty)))); + (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c)))); Genprint.register_print0 Constrarg.wit_clause_dft_concl (pr_clauses (Some true) pr_lident) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index fa91aefcf..30b9483db 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -48,7 +48,7 @@ type pp_tactic = { pptac_prods : int * grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 166a6675c..1631bda37 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -59,19 +59,19 @@ module type Pp = sig (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> int -> - ml_tactic_name -> raw_generic_argument list -> std_ppcmds + ml_tactic_entry -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_name -> glob_generic_argument list -> std_ppcmds + ml_tactic_entry -> glob_generic_argument list -> std_ppcmds val pr_extend : (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (constr_pattern -> std_ppcmds) -> int -> - ml_tactic_name -> typed_generic_argument list -> std_ppcmds + ml_tactic_entry -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds |