From d5d15af811a487e65f8c10dfb68d5608f3722f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 30 Nov 2013 18:58:57 +0100 Subject: Adding printing of ltac envs to debugger. --- dev/db | 1 + dev/top_printers.ml | 19 ++++++++++++++----- 2 files changed, 15 insertions(+), 5 deletions(-) (limited to 'dev') diff --git a/dev/db b/dev/db index 10926be086..88cd9b057b 100644 --- a/dev/db +++ b/dev/db @@ -39,3 +39,4 @@ install_printer Top_printers.prsubst install_printer Top_printers.prdelta install_printer Top_printers.ppfconstr install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppist diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3d90d25cf3..c2cbfae160 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -65,9 +65,12 @@ let ppintset l = pp (prset int (Int.Set.elements l)) let ppidset l = pp (prset pr_id (Id.Set.elements l)) let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" -let ppidmap pr l = + +let pridmap pr l = let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in - pp (prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])) + prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) + +let ppidmap pr l = pp (pridmap pr l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 @@ -355,14 +358,20 @@ let pp_argument_type t = pp (pr_argument_type t) let pp_generic_argument arg = pp(str"") -let ppgenarginfo arg = +let prgenarginfo arg = let tpe = pr_argument_type (genarg_tag arg) in let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in try let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in - pp (str "") + str "" with _any -> - pp (str "") + str "" + +let ppgenarginfo arg = pp (prgenarginfo arg) + +let ppist ist = + let pr id arg = prgenarginfo arg in + pp (pridmap pr ist.Geninterp.lfun) (**********************************************************************) (* Vernac-level debugging commands *) -- cgit v1.2.3