diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
3 files changed, 5 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 792330726b..83e23d29f5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -19,6 +19,7 @@ #install_printer (* identifier *) ppid;; #install_printer (* identifier *) ppidset;; +#install_printer (* Intset.t *) ppintset;; #install_printer (* label *) pplab;; #install_printer (* mod_self_id *) ppmsid;; #install_printer (* mod_bound_id *) ppmbid;; @@ -3,6 +3,7 @@ load_printer "printers.cma" install_printer Top_printers.ppid install_printer Top_printers.ppidset +install_printer Top_printers.ppintset 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 07dda42b85..c06738226b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -62,7 +62,9 @@ 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 prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]" +let ppintset l = pp (prset int (Intset.elements l)) +let ppidset l = pp (prset pr_id (Idset.elements l)) let pP s = pp (hov 0 s) |