diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:01:26 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:01:26 +0000 |
| commit | d9e885515da1592075f5599290e6117c095216b4 (patch) | |
| tree | 8ffa7e3c045166abae5a46f8d83efa80dca1ee37 /lib/pp.mli | |
| parent | c9f997fd32e3bccf58b9d3c26e1822a765c44d21 (diff) | |
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
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 4e64925fd..d4248cc7f 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 |