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
(* $Id: pp.ml4 10803 2008-04-16 09:30:05Z cek $ *)
13
(* This should not be used outside of this file. Use
14
Flags.print_emacs instead. This one is updated when reading
15
command line options. This was the only way to make [Pp] depend on
16
an option without creating a circularity: [Flags. -> [Util] ->
18
let print_emacs = ref false
19
let make_pp_emacs() = print_emacs:=true
20
let make_pp_nonemacs() = print_emacs:=false
22
(* The different kinds of blocks are:
24
\item[hbox:] Horizontal block no line breaking;
25
\item[vbox:] Vertical block each break leads to a new line;
26
\item[hvbox:] Horizontal-vertical block: same as vbox, except if
27
this block is small enough to fit on a single line
28
\item[hovbox:] Horizontal or Vertical block: breaks lead to new line
29
only when necessary to print the content of the block
30
\item[tbox:] Tabulation block: go to tabulation marks and no line breaking
31
(except if no mark yet on the reste of the line)
37
let rec split_com comacc acc pos = function
38
[] -> comments := List.rev acc; comacc
39
| ((b,e),c as com)::coms ->
40
(* Take all comments that terminates before pos, or begin exactly
41
at pos (used to print comments attached after an expression) *)
42
if e<=pos || pos=b then split_com (c::comacc) acc pos coms
43
else split_com comacc (com::acc) pos coms
55
| Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
56
| Ppcmd_print_break of int * int
58
| Ppcmd_print_tbreak of int * int
59
| Ppcmd_white_space of int
61
| Ppcmd_print_if_broken
62
| Ppcmd_open_box of block_type
65
| Ppcmd_comment of int
68
| Ppdir_ppcmds of 'a ppcmd_token Stream.t
72
type ppcmd = (int*string) ppcmd_token
74
type std_ppcmds = ppcmd Stream.t
76
type 'a ppdirs = 'a ppdir_token Stream.t
78
(* Compute length of an UTF-8 encoded string
79
Rem 1 : utf8_length <= String.length (equal if pure ascii)
80
Rem 2 : if used for an iso8859_1 encoded string, the result is
81
wrong in very rare cases. Such a wrong case corresponds to any
82
sequence of a character in range 192..253 immediately followed by a
83
character in range 128..191 (typical case in french is "d��u" which
84
is counted 3 instead of 4); then no real harm to use always
85
utf8_length even if using an iso8859_1 encoding *)
88
let len = String.length s
95
| '\000'..'\127' -> nc := 0 (* ascii char *)
96
| '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
97
| '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
98
| '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
99
| '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
100
| '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
101
| '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
102
| '\254'..'\255' -> nc := 0 (* invalid byte *)
105
while !p < len && !nc > 0 do
107
| '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
108
| _ (* not a continuation byte *) -> nc := 0
114
(* formatting commands *)
115
let str s = [< 'Ppcmd_print (utf8_length s,s) >]
116
let stras (i,s) = [< 'Ppcmd_print (i,s) >]
117
let brk (a,b) = [< 'Ppcmd_print_break (a,b) >]
118
let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >]
119
let tab () = [< 'Ppcmd_set_tab >]
120
let fnl () = [< 'Ppcmd_force_newline >]
121
let pifb () = [< 'Ppcmd_print_if_broken >]
122
let ws n = [< 'Ppcmd_white_space n >]
123
let comment n = [< ' Ppcmd_comment n >]
125
(* derived commands *)
127
let spc () = [< 'Ppcmd_print_break (1,0) >]
128
let cut () = [< 'Ppcmd_print_break (0,0) >]
129
let align () = [< 'Ppcmd_print_break (0,0) >]
130
let int n = str (string_of_int n)
131
let real r = str (string_of_float r)
132
let bool b = str (string_of_bool b)
135
if n < String.length s then
137
if p=n then [< spc (); aux (n+1) (n+1) >]
138
else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >]
140
else if p=n then [< >] else [< str (String.sub s p (n-p)) >]
143
let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false
145
(* boxing commands *)
146
let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
147
let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
148
let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
149
let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
150
let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
152
(* Opening and closing of boxes *)
153
let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >]
154
let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >]
155
let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >]
156
let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >]
157
let tb () = [< 'Ppcmd_open_box Pp_tbox >]
158
let close () = [< 'Ppcmd_close_box >]
159
let tclose () = [< 'Ppcmd_close_tbox >]
161
let (++) = Stream.iapp
163
(* In new syntax only double quote char is escaped by repeating it *)
164
let rec escape_string s =
165
let rec escape_at s i =
167
else if s.[i] == '"' then
168
let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
170
else escape_at s (i-1) in
171
escape_at s (String.length s - 1)
173
let qstring s = str ("\""^escape_string s^"\"")
175
let quote s = h 0 (str "\"" ++ s ++ str "\"")
177
let rec xmlescape ppcmd =
178
let rec escape what withwhat (len, str) =
180
let pos = String.index str what in
182
escape what withwhat ((len - pos - 1),
183
(String.sub str (pos + 1) (len - pos - 1)))
185
(pos + tlen + String.length withwhat, String.sub str 0 pos ^ withwhat ^ tail)
186
with Not_found -> (len, str)
189
| Ppcmd_print (len, str) ->
190
Ppcmd_print (escape '"' """
191
(escape '<' "<" (escape '&' "&" (len, str))))
192
(* In XML we always print whole content so we can npeek the whole stream *)
193
| Ppcmd_box (x, str) -> Ppcmd_box (x, Stream.of_list
194
(List.map xmlescape (Stream.npeek max_int str)))
198
(* This flag tells if the last printed comment ends with a newline, to
200
let com_eol = ref false
202
let com_brk ft = com_eol := false
204
if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
207
let rec pr_com ft s =
210
let n = String.index s '\n' in
211
String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
212
with Not_found -> s,None in
213
com_if ft (Lazy.lazy_from_val());
215
if String.length s1 <> 0 && s1.[0] = ' ' then
216
(Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
218
Format.pp_print_as ft (utf8_length s1) s1;
221
if String.length s2 = 0 then (com_eol := true)
223
(Format.pp_force_newline ft (); pr_com ft s2)
226
(* pretty printing functions *)
228
let pp_open_box = function
229
| Pp_hbox n -> Format.pp_open_hbox ft ()
230
| Pp_vbox n -> Format.pp_open_vbox ft n
231
| Pp_hvbox n -> Format.pp_open_hvbox ft n
232
| Pp_hovbox n -> Format.pp_open_hovbox ft n
233
| Pp_tbox -> Format.pp_open_tbox ft ()
235
let rec pp_cmd = function
236
| Ppcmd_print(n,s) ->
237
com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
238
| Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *)
239
com_if ft (Lazy.lazy_from_val());
241
if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
242
Format.pp_close_box ft ()
243
| Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
244
| Ppcmd_close_box -> Format.pp_close_box ft ()
245
| Ppcmd_close_tbox -> Format.pp_close_tbox ft ()
246
| Ppcmd_white_space n ->
247
com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
248
| Ppcmd_print_break(m,n) ->
249
com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
250
| Ppcmd_set_tab -> Format.pp_set_tab ft ()
251
| Ppcmd_print_tbreak(m,n) ->
252
com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
253
| Ppcmd_force_newline ->
254
com_brk ft; Format.pp_force_newline ft ()
255
| Ppcmd_print_if_broken ->
256
com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
258
let coms = split_com [] [] i !comments in
259
(* Format.pp_open_hvbox ft 0;*)
260
List.iter (pr_com ft) coms(*;
261
Format.pp_close_box ft ()*)
263
let pp_dir = function
264
| Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
265
| Ppdir_print_newline ->
266
com_brk ft; Format.pp_print_newline ft ()
267
| Ppdir_print_flush -> Format.pp_print_flush ft ()
271
Stream.iter pp_dir dirstream; com_brk ft
273
| e -> Format.pp_print_flush ft () ; raise e
276
(* pretty print on stdout and stderr *)
278
let pp_std_dirs = pp_dirs !std_ft
279
let pp_err_dirs = pp_dirs !err_ft
281
let ppcmds x = Ppdir_ppcmds x
283
(* Special chars for emacs, to detect warnings inside goal output *)
284
let emacs_warning_start_string = String.make 1 (Char.chr 254)
285
let emacs_warning_end_string = String.make 1 (Char.chr 255)
288
if not !print_emacs then mt() else str emacs_warning_start_string
291
if not !print_emacs then mt() else str emacs_warning_end_string
294
[< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
296
(* pretty printing functions WITHOUT FLUSH *)
297
let pp_with ft strm =
298
pp_dirs ft [< 'Ppdir_ppcmds strm >]
300
let ppnl_with ft strm =
301
pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
303
let default_warn_with ft strm = ppnl_with ft (warnbody strm)
305
let pp_warn_with = ref default_warn_with
307
let set_warning_function pp_warn = pp_warn_with := pp_warn
309
let warn_with ft strm = !pp_warn_with ft strm
311
let warning_with ft string = warn_with ft (str string)
313
let pp_flush_with ft = Format.pp_print_flush ft
315
(* pretty printing functions WITH FLUSH *)
316
let msg_with ft strm =
317
pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >]
319
let msgnl_with ft strm =
320
pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
322
let msg_warning_with ft strm =
323
msgnl_with ft (warnbody strm)
325
(* pretty printing functions WITHOUT FLUSH *)
326
let pp x = pp_with !std_ft x
327
let ppnl x = ppnl_with !std_ft x
328
let pperr x = pp_with !err_ft x
329
let pperrnl x = ppnl_with !err_ft x
330
let message s = ppnl (str s)
331
let warning x = warning_with !err_ft x
332
let warn x = warn_with !err_ft x
333
let pp_flush x = Format.pp_print_flush !std_ft x
334
let flush_all() = flush stderr; flush stdout; pp_flush()
336
(* pretty printing functions WITH FLUSH *)
337
let msg x = msg_with !std_ft x
338
let msgnl x = msgnl_with !std_ft x
339
let msgerr x = msg_with !err_ft x
340
let msgerrnl x = msgnl_with !err_ft x
341
let msg_warning x = msg_warning_with !err_ft x
added
removed
lib/pp.ml4
