From d9e885515da1592075f5599290e6117c095216b4 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Thu, 27 Apr 2006 16:01:26 +0000
Subject: Modification of emacs output: Pp.warning and al now output warning
 between special characters.

I had to add a hidden variable print_emacs and a function to set it to
true in Pp because using Options.print_emacs would have introduce a
circularity.
 

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/pp.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib')

diff --git a/lib/pp.mli b/lib/pp.mli
index 4e64925fdf..d4248cc7f2 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,11 @@
 open Pp_control
 (*i*)
 
+(* Modify pretty printing functions behavior for emacs ouput (special
+   chars inserted at some places). This function should called once in
+   module [Options], that's all. *)
+val make_pp_emacs:unit -> unit
+
 (* Pretty-printers. *)
 
 type ppcmd
-- 
cgit v1.2.3