aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-11-30 18:58:57 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-11-30 18:58:57 +0100
commitd5d15af811a487e65f8c10dfb68d5608f3722f8a (patch)
treec4b715bff21c6bb78f950b0452bfcc2945b33062
parenta01a60b366307da3eca63c9937984db6f273dc41 (diff)
Adding printing of ltac envs to debugger.
-rw-r--r--dev/db1
-rw-r--r--dev/top_printers.ml19
2 files changed, 15 insertions, 5 deletions
diff --git a/dev/db b/dev/db
index 10926be08..88cd9b057 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 3d90d25cf..c2cbfae16 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"<genarg:"++pr_argument_type(genarg_tag arg)++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 "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >")
+ str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
with _any ->
- pp (str "<genarg:" ++ tpe ++ str ">")
+ str "<genarg:" ++ tpe ++ 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 *)