aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-04-25 14:36:19 +0200
committerPierre-Marie Pédrot2014-04-25 14:39:15 +0200
commit38d2881dcd1917a93b202c16a55d57d51006ee88 (patch)
treec3995446d077b16a55367e52af4d45013707b805 /dev
parentb35edb34769fecd4dbdf7030222ba3078eab1c93 (diff)
Adding a debug printer for futures.
Diffstat (limited to 'dev')
-rw-r--r--dev/db2
-rw-r--r--dev/top_printers.ml4
2 files changed, 6 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index 4777a53484..fc63e51114 100644
--- a/dev/db
+++ b/dev/db
@@ -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)