1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: pp.mli 10803 2008-04-16 09:30:05Z cek $ i*)
15
(* Modify pretty printing functions behavior for emacs ouput (special
16
chars inserted at some places). This function should called once in
17
module [Options], that's all. *)
18
val make_pp_emacs:unit -> unit
19
val make_pp_nonemacs:unit -> unit
21
(* Pretty-printers. *)
25
type std_ppcmds = ppcmd Stream.t
27
(*s Formatting commands. *)
29
val str : string -> std_ppcmds
30
val stras : int * string -> std_ppcmds
31
val brk : int * int -> std_ppcmds
32
val tbrk : int * int -> std_ppcmds
33
val tab : unit -> std_ppcmds
34
val fnl : unit -> std_ppcmds
35
val pifb : unit -> std_ppcmds
36
val ws : int -> std_ppcmds
37
val mt : unit -> std_ppcmds
38
val ismt : std_ppcmds -> bool
40
val comment : int -> std_ppcmds
41
val comments : ((int * int) * string) list ref
45
val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
47
(*s Derived commands. *)
49
val spc : unit -> std_ppcmds
50
val cut : unit -> std_ppcmds
51
val align : unit -> std_ppcmds
52
val int : int -> std_ppcmds
53
val real : float -> std_ppcmds
54
val bool : bool -> std_ppcmds
55
val qstring : string -> std_ppcmds
56
val qs : string -> std_ppcmds
57
val quote : std_ppcmds -> std_ppcmds
58
val strbrk : string -> std_ppcmds
60
val xmlescape : ppcmd -> ppcmd
62
(*s Boxing commands. *)
64
val h : int -> std_ppcmds -> std_ppcmds
65
val v : int -> std_ppcmds -> std_ppcmds
66
val hv : int -> std_ppcmds -> std_ppcmds
67
val hov : int -> std_ppcmds -> std_ppcmds
68
val t : std_ppcmds -> std_ppcmds
70
(*s Opening and closing of boxes. *)
72
val hb : int -> std_ppcmds
73
val vb : int -> std_ppcmds
74
val hvb : int -> std_ppcmds
75
val hovb : int -> std_ppcmds
76
val tb : unit -> std_ppcmds
77
val close : unit -> std_ppcmds
78
val tclose : unit -> std_ppcmds
80
(*s Pretty-printing functions \emph{without flush}. *)
82
val pp_with : Format.formatter -> std_ppcmds -> unit
83
val ppnl_with : Format.formatter -> std_ppcmds -> unit
84
val warning_with : Format.formatter -> string -> unit
85
val warn_with : Format.formatter -> std_ppcmds -> unit
86
val pp_flush_with : Format.formatter -> unit -> unit
88
val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
90
(*s Pretty-printing functions \emph{with flush}. *)
92
val msg_with : Format.formatter -> std_ppcmds -> unit
93
val msgnl_with : Format.formatter -> std_ppcmds -> unit
96
(*s The following functions are instances of the previous ones on
97
[std_ft] and [err_ft]. *)
99
(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
101
val pp : std_ppcmds -> unit
102
val ppnl : std_ppcmds -> unit
103
val pperr : std_ppcmds -> unit
104
val pperrnl : std_ppcmds -> unit
105
val message : string -> unit (* = pPNL *)
106
val warning : string -> unit
107
val warn : std_ppcmds -> unit
108
val pp_flush : unit -> unit
109
val flush_all: unit -> unit
111
(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
113
val msg : std_ppcmds -> unit
114
val msgnl : std_ppcmds -> unit
115
val msgerr : std_ppcmds -> unit
116
val msgerrnl : std_ppcmds -> unit
117
val msg_warning : std_ppcmds -> unit