From 6c0af6104d41762220a1d613d2331e7a0294df80 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 14 Nov 2011 16:38:19 +0000
Subject: Bug 2636 - Move string_of_ppcmds to Pp

by Tom Prince

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/pp.ml4 | 4 ++++
 lib/pp.mli | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 854e4b49ca..c602b403e0 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -332,3 +332,7 @@ let msgnl x = msgnl_with !std_ft x
 let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
+
+let string_of_ppcmds c =
+  msg_with Format.str_formatter c;
+  Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 44732c7efb..7070e3f5f4 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -112,3 +112,5 @@ val msgnl : std_ppcmds -> unit
 val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
+
+val string_of_ppcmds : std_ppcmds -> string
-- 
cgit v1.2.3