summaryrefslogtreecommitdiff
path: root/lib/pp.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'lib/pp.ml4')
-rw-r--r--lib/pp.ml4287
1 files changed, 287 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4
new file mode 100644
index 00000000..25ab9ce8
--- /dev/null
+++ b/lib/pp.ml4
@@ -0,0 +1,287 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: pp.ml4,v 1.5.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+open Pp_control
+
+(* The different kinds of blocks are:
+ \begin{description}
+ \item[hbox:] Horizontal block no line breaking;
+ \item[vbox:] Vertical block each break leads to a new line;
+ \item[hvbox:] Horizontal-vertical block: same as vbox, except if
+ this block is small enough to fit on a single line
+ \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
+ only when necessary to print the content of the block
+ \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
+ (except if no mark yet on the reste of the line)
+ \end{description}
+ *)
+
+let comments = ref []
+
+let rec split_com comacc acc pos = function
+ [] -> comments := List.rev acc; comacc
+ | ((b,e),c as com)::coms ->
+ (* Take all comments that terminates before pos, or begin exactly
+ at pos (used to print comments attached after an expression) *)
+ if e<=pos || pos=b then split_com (c::comacc) acc pos coms
+ else split_com comacc (com::acc) pos coms
+
+
+type block_type =
+ | Pp_hbox of int
+ | Pp_vbox of int
+ | Pp_hvbox of int
+ | Pp_hovbox of int
+ | Pp_tbox
+
+type 'a ppcmd_token =
+ | Ppcmd_print of 'a
+ | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
+ | Ppcmd_print_break of int * int
+ | Ppcmd_set_tab
+ | Ppcmd_print_tbreak of int * int
+ | Ppcmd_white_space of int
+ | Ppcmd_force_newline
+ | Ppcmd_print_if_broken
+ | Ppcmd_open_box of block_type
+ | Ppcmd_close_box
+ | Ppcmd_close_tbox
+ | Ppcmd_comment of int
+
+type 'a ppdir_token =
+ | Ppdir_ppcmds of 'a ppcmd_token Stream.t
+ | Ppdir_print_newline
+ | Ppdir_print_flush
+
+type ppcmd = (int*string) ppcmd_token
+
+type std_ppcmds = ppcmd Stream.t
+
+type 'a ppdirs = 'a ppdir_token Stream.t
+
+(* Compute length of an UTF-8 encoded string
+ Rem 1 : utf8_length <= String.length (equal if pure ascii)
+ Rem 2 : if used for an iso8859_1 encoded string, the result is
+ wrong in very rare cases. Such a wrong case corresponds to any
+ sequence of a character in range 192..253 immediately followed by a
+ character in range 128..191 (typical case in french is "déçu" which
+ is counted 3 instead of 4); then no real harm to use always
+ utf8_length even if using an iso8859_1 encoding *)
+
+let utf8_length s =
+ let len = String.length s
+ and cnt = ref 0
+ and nc = ref 0
+ and p = ref 0 in
+ while !p < len do
+ begin
+ match s.[!p] with
+ | '\000'..'\127' -> nc := 0 (* ascii char *)
+ | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
+ | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
+ | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
+ | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
+ | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
+ | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
+ | '\254'..'\255' -> nc := 0 (* invalid byte *)
+ end ;
+ incr p ;
+ while !p < len && !nc > 0 do
+ match s.[!p] with
+ | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
+ | _ (* not a continuation byte *) -> nc := 0
+ done ;
+ incr cnt
+ done ;
+ !cnt
+
+(* formatting commands *)
+let str s = [< 'Ppcmd_print (utf8_length s,s) >]
+let stras (i,s) = [< 'Ppcmd_print (i,s) >]
+let brk (a,b) = [< 'Ppcmd_print_break (a,b) >]
+let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >]
+let tab () = [< 'Ppcmd_set_tab >]
+let fnl () = [< 'Ppcmd_force_newline >]
+let pifb () = [< 'Ppcmd_print_if_broken >]
+let ws n = [< 'Ppcmd_white_space n >]
+let comment n = [< ' Ppcmd_comment n >]
+
+(* derived commands *)
+let mt () = [< >]
+let spc () = [< 'Ppcmd_print_break (1,0) >]
+let cut () = [< 'Ppcmd_print_break (0,0) >]
+let align () = [< 'Ppcmd_print_break (0,0) >]
+let int n = str (string_of_int n)
+let real r = str (string_of_float r)
+let bool b = str (string_of_bool b)
+
+let rec escape_string s =
+ let rec escape_at s i =
+ if i<0 then s
+ else if s.[i] == '\\' || s.[i] == '"' then
+ let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in
+ escape_at s' (i-1)
+ else escape_at s (i-1) in
+ escape_at s (String.length s - 1)
+
+
+let qstring s = str ("\""^(escape_string s)^"\"")
+let qs = qstring
+
+(* boxing commands *)
+let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
+let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
+let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
+let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
+let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
+
+(* Opening and closing of boxes *)
+let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >]
+let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >]
+let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >]
+let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >]
+let tb () = [< 'Ppcmd_open_box Pp_tbox >]
+let close () = [< 'Ppcmd_close_box >]
+let tclose () = [< 'Ppcmd_close_tbox >]
+
+let (++) = Stream.iapp
+
+(* This flag tells if the last printed comment ends with a newline, to
+ avoid empty lines *)
+let com_eol = ref false
+
+let com_brk ft = com_eol := false
+let com_if ft f =
+ if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
+ else Lazy.force f
+
+let rec pr_com ft s =
+ let (s1,os) =
+ try
+ let n = String.index s '\n' in
+ String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
+ with Not_found -> s,None in
+ com_if ft (Lazy.lazy_from_val());
+(* let s1 =
+ if String.length s1 <> 0 && s1.[0] = ' ' then
+ (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
+ else s1 in*)
+ Format.pp_print_as ft (utf8_length s1) s1;
+ match os with
+ Some s2 ->
+ if String.length s2 = 0 then (com_eol := true)
+ else
+ (Format.pp_force_newline ft (); pr_com ft s2)
+ | None -> ()
+
+(* pretty printing functions *)
+let pp_dirs ft =
+ let maxbox = (get_gp ft).max_depth in
+ let pp_open_box = function
+ | Pp_hbox n -> Format.pp_open_hbox ft ()
+ | Pp_vbox n -> Format.pp_open_vbox ft n
+ | Pp_hvbox n -> Format.pp_open_hvbox ft n
+ | Pp_hovbox n -> Format.pp_open_hovbox ft n
+ | Pp_tbox -> Format.pp_open_tbox ft ()
+ in
+ let rec pp_cmd = function
+ | Ppcmd_print(n,s) ->
+ com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+ | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *)
+ com_if ft (Lazy.lazy_from_val());
+ pp_open_box bty ;
+ if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
+ Format.pp_close_box ft ()
+ | Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
+ | Ppcmd_close_box -> Format.pp_close_box ft ()
+ | Ppcmd_close_tbox -> Format.pp_close_tbox ft ()
+ | Ppcmd_white_space n ->
+ com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+ | Ppcmd_print_break(m,n) ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+ | Ppcmd_set_tab -> Format.pp_set_tab ft ()
+ | Ppcmd_print_tbreak(m,n) ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+ | Ppcmd_force_newline ->
+ com_brk ft; Format.pp_force_newline ft ()
+ | Ppcmd_print_if_broken ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
+ | Ppcmd_comment i ->
+ let coms = split_com [] [] i !comments in
+(* Format.pp_open_hvbox ft 0;*)
+ List.iter (pr_com ft) coms(*;
+ Format.pp_close_box ft ()*)
+ in
+ let pp_dir = function
+ | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
+ | Ppdir_print_newline ->
+ com_brk ft; Format.pp_print_newline ft ()
+ | Ppdir_print_flush -> Format.pp_print_flush ft ()
+ in
+ fun dirstream ->
+ try
+ Stream.iter pp_dir dirstream; com_brk ft
+ with
+ | e -> Format.pp_print_flush ft () ; raise e
+
+
+(* pretty print on stdout and stderr *)
+
+let pp_std_dirs = pp_dirs !std_ft
+let pp_err_dirs = pp_dirs err_ft
+
+let ppcmds x = Ppdir_ppcmds x
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pp_with ft strm =
+ pp_dirs ft [< 'Ppdir_ppcmds strm >]
+
+let ppnl_with ft strm =
+ pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
+
+let warning_with ft string =
+ ppnl_with ft [< str "Warning: " ; str string >]
+
+let warn_with ft pps =
+ ppnl_with ft [< str "Warning: " ; pps >]
+
+let pp_flush_with ft =
+ Format.pp_print_flush ft
+
+
+(* pretty printing functions WITH FLUSH *)
+let msg_with ft strm =
+ pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >]
+
+let msgnl_with ft strm =
+ pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
+
+let msg_warning_with ft strm=
+ pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>];
+ 'Ppdir_print_newline >]
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pp x = pp_with !std_ft x
+let ppnl x = ppnl_with !std_ft x
+let pperr = pp_with err_ft
+let pperrnl = ppnl_with err_ft
+let message s = ppnl (str s)
+let warning x = warning_with err_ft x
+let warn x = warn_with err_ft x
+let pp_flush x = Format.pp_print_flush !std_ft x
+let flush_all() = flush stderr; flush stdout; pp_flush()
+
+(* pretty printing functions WITH FLUSH *)
+let msg x = msg_with !std_ft x
+let msgnl x = msgnl_with !std_ft x
+let msgerr = msg_with err_ft
+let msgerrnl = msgnl_with err_ft
+let msg_warning x = msg_warning_with err_ft x
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 23:49:07 +0000