diff options
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 5 |
3 files changed, 5 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include index cd837ab6a..30a6ed96d 100644 --- a/dev/base_include +++ b/dev/base_include @@ -18,6 +18,7 @@ #use "vm_printers.ml";; #install_printer (* identifier *) ppid;; +#install_printer (* identifier *) ppidset;; #install_printer (* label *) pplab;; #install_printer (* mod_self_id *) ppmsid;; #install_printer (* mod_bound_id *) ppmbid;; @@ -2,6 +2,7 @@ load_printer "gramlib.cma" load_printer "printers.cma" install_printer Top_printers.ppid +install_printer Top_printers.ppidset install_printer Top_printers.pplab install_printer Top_printers.ppmsid install_printer Top_printers.ppmbid diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f4f17c1d7..1cd2369e6 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -9,6 +9,7 @@ (* Printers for the ocaml toplevel. *) open System +open Util open Pp open Names open Libnames @@ -52,6 +53,8 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let ppbigint n = pp (Bigint.pr_bigint n);; +let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l)) + let pP s = pp (hov 0 s) let safe_pr_global = function @@ -83,8 +86,6 @@ let ppgoal g = pp(db_pr_goal g) let pr_gls gls = hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) -open Util - let pr_glls glls = hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) |