diff options
| author | Pierre-Marie Pédrot | 2014-04-25 14:36:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:39:15 +0200 |
| commit | 38d2881dcd1917a93b202c16a55d57d51006ee88 (patch) | |
| tree | c3995446d077b16a55367e52af4d45013707b805 /dev | |
| parent | b35edb34769fecd4dbdf7030222ba3078eab1c93 (diff) | |
Adding a debug printer for futures.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 6 insertions, 0 deletions
@@ -2,6 +2,8 @@ load_printer "gramlib.cma" load_printer "str.cma" load_printer "printers.cma" +install_printer Top_printers.ppfuture + install_printer Top_printers.ppid install_printer Top_printers.ppidset install_printer Top_printers.ppevar diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6f2c241767..7d6370b9d5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -31,6 +31,10 @@ let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) let pppp x = pp x +(** Future printer *) + +let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) + (* name printers *) let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) |
