blob: 09efc57a1d29b1e5cb86affd9b880711a74e4542 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp_control
open Compat
(** 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
val make_pp_nonemacs:unit -> unit
(** Pretty-printers. *)
type ppcmd
type std_ppcmds = ppcmd Stream.t
(** {6 Formatting commands. } *)
val str : string -> std_ppcmds
val stras : int * string -> std_ppcmds
val brk : int * int -> std_ppcmds
val tbrk : int * int -> std_ppcmds
val tab : unit -> std_ppcmds
val fnl : unit -> std_ppcmds
val pifb : unit -> std_ppcmds
val ws : int -> std_ppcmds
val mt : unit -> std_ppcmds
val ismt : std_ppcmds -> bool
val comment : int -> std_ppcmds
val comments : ((int * int) * string) list ref
(** {6 Concatenation. } *)
val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
(** {6 Evaluation. } *)
val eval_ppcmds : std_ppcmds -> std_ppcmds
(** {6 Derived commands. } *)
val spc : unit -> std_ppcmds
val cut : unit -> std_ppcmds
val align : unit -> std_ppcmds
val int : int -> std_ppcmds
val real : float -> std_ppcmds
val bool : bool -> std_ppcmds
val qstring : string -> std_ppcmds
val qs : string -> std_ppcmds
val quote : std_ppcmds -> std_ppcmds
val strbrk : string -> std_ppcmds
val xmlescape : ppcmd -> ppcmd
(** {6 Boxing commands. } *)
val h : int -> std_ppcmds -> std_ppcmds
val v : int -> std_ppcmds -> std_ppcmds
val hv : int -> std_ppcmds -> std_ppcmds
val hov : int -> std_ppcmds -> std_ppcmds
val t : std_ppcmds -> std_ppcmds
(** {6 Opening and closing of boxes. } *)
val hb : int -> std_ppcmds
val vb : int -> std_ppcmds
val hvb : int -> std_ppcmds
val hovb : int -> std_ppcmds
val tb : unit -> std_ppcmds
val close : unit -> std_ppcmds
val tclose : unit -> std_ppcmds
(** {6 Sending messages to the user } *)
type level =
| Debug of string
| Info
| Notice
| Warning
| Error
type logger = level -> std_ppcmds -> unit
val msg_info : std_ppcmds -> unit
(** Message that displays information, usually in verbose mode, such as [Foobar
is defined] *)
val msg_notice : std_ppcmds -> unit
(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
val msg_warning : std_ppcmds -> unit
(** Message indicating that something went wrong, but without serious
consequences. *)
val msg_error : std_ppcmds -> unit
(** Message indicating that something went really wrong, though still
recoverable; otherwise an exception would have been raised. *)
val msg_debug : std_ppcmds -> unit
(** For debugging purposes *)
val std_logger : logger
(** Standard logging function *)
val set_logger : logger -> unit
(** {6 Utilities} *)
val string_of_ppcmds : std_ppcmds -> string
(** {6 Deprecated functions} *)
(** DEPRECATED. Do not use in newly written code. *)
val msg : std_ppcmds -> unit
val msgnl : std_ppcmds -> unit
val msgerr : std_ppcmds -> unit
val msgerrnl : std_ppcmds -> unit
val message : string -> unit (** = pPNL *)
(** {6 Location management. } *)
type loc = Loc.t
val unloc : loc -> int * int
val make_loc : int * int -> loc
val dummy_loc : loc
val join_loc : loc -> loc -> loc
type 'a located = loc * 'a
val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
val down_located : ('a -> 'b) -> 'a located -> 'b
(** {6 Util copy/paste. } *)
val pr_comma : unit -> std_ppcmds
val pr_semicolon : unit -> std_ppcmds
val pr_bar : unit -> std_ppcmds
val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
val pr_nth : int -> std_ppcmds
val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(** unlike all other functions below, [prlist] works lazily.
if a strict behavior is needed, use [prlist_strict] instead. *)
val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val prlist_with_sep :
(unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
val prvect_with_sep :
(unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
val prvecti_with_sep :
(unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val surround : std_ppcmds -> std_ppcmds
(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
val pp_with : Format.formatter -> std_ppcmds -> unit
val ppnl_with : Format.formatter -> std_ppcmds -> unit
val pp_flush_with : Format.formatter -> unit -> unit
(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
(** These functions are low-level interface to printing and should not be used
in usual code. Consider using the [msg_*] function family instead. *)
val pp : std_ppcmds -> unit
val ppnl : std_ppcmds -> unit
val pperr : std_ppcmds -> unit
val pperrnl : std_ppcmds -> unit
val pperr_flush : unit -> unit
val pp_flush : unit -> unit
val flush_all: unit -> unit
(** {6 Low-level pretty-printing functions {% \emph{%}with flush{% }%}. } *)
val msg_with : Format.formatter -> std_ppcmds -> unit
|
