From 38d2881dcd1917a93b202c16a55d57d51006ee88 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Apr 2014 14:36:19 +0200
Subject: Adding a debug printer for futures.

---
 dev/db              | 2 ++
 dev/top_printers.ml | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'dev')

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)
-- 
cgit v1.2.3