1995-08-09 08:06:35 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
2011-07-27 07:17:02 -07:00
|
|
|
(* OCaml *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
1997-11-06 06:11:06 -08:00
|
|
|
(* Pierre Weis, projet Cristal, INRIA Rocquencourt *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
1999-11-17 10:59:06 -08:00
|
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
2001-12-07 05:41:02 -08:00
|
|
|
(* under the terms of the GNU Library General Public License, with *)
|
|
|
|
(* the special exception on linking described in file ../LICENSE. *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
2007-05-08 14:30:01 -07:00
|
|
|
(* A pretty-printing facility and definition of formatters for ``parallel''
|
|
|
|
(i.e. unrelated or independent) pretty-printing on multiple out channels. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Data structures definitions.
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
type size;;
|
|
|
|
|
2008-06-16 06:04:46 -07:00
|
|
|
external size_of_int : int -> size = "%identity"
|
|
|
|
;;
|
|
|
|
external int_of_size : size -> int = "%identity"
|
|
|
|
;;
|
2005-09-20 10:18:03 -07:00
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
(* Tokens are one of the following : *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
type pp_token =
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_text of string (* normal text *)
|
|
|
|
| Pp_break of int * int (* complete break *)
|
2002-03-11 14:18:20 -08:00
|
|
|
| Pp_tbreak of int * int (* go to next tabulation *)
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_stab (* set a tabulation *)
|
|
|
|
| Pp_begin of int * block_type (* beginning of a block *)
|
|
|
|
| Pp_end (* end of a block *)
|
2002-03-11 14:18:20 -08:00
|
|
|
| Pp_tbegin of tblock (* beginning of a tabulation block *)
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_tend (* end of a tabulation block *)
|
|
|
|
| Pp_newline (* to force a newline inside a block *)
|
|
|
|
| Pp_if_newline (* to do something only if this very
|
|
|
|
line has been broken *)
|
2012-04-27 02:56:05 -07:00
|
|
|
| Pp_open_tag of tag (* opening a tag name *)
|
2002-05-15 13:29:26 -07:00
|
|
|
| Pp_close_tag (* closing the most recently opened tag *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
and tag = string
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
and block_type =
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_hbox (* Horizontal block no line breaking *)
|
|
|
|
| Pp_vbox (* Vertical block each break leads to a new line *)
|
|
|
|
| Pp_hvbox (* Horizontal-vertical block: same as vbox, except if this block
|
|
|
|
is small enough to fit on a single line *)
|
|
|
|
| Pp_hovbox (* Horizontal or Vertical block: breaks lead to new line
|
|
|
|
only when necessary to print the content of the block *)
|
|
|
|
| Pp_box (* Horizontal or Indent block: breaks lead to new line
|
|
|
|
only when necessary to print the content of the block, or
|
|
|
|
when it leads to a new indentation of the current line *)
|
|
|
|
| Pp_fits (* Internal usage: when a block fits on a single line *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2011-06-20 14:46:20 -07:00
|
|
|
and tblock =
|
|
|
|
| Pp_tbox of int list ref (* Tabulation box *)
|
1996-07-08 11:53:26 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(* The Queue:
|
|
|
|
contains all formatting elements.
|
1997-10-23 00:53:12 -07:00
|
|
|
elements are tuples (size, token, length), where
|
1995-05-04 03:15:53 -07:00
|
|
|
size is set when the size of the block is known
|
2004-03-05 04:15:31 -08:00
|
|
|
len is the declared length of the token. *)
|
2005-09-20 10:18:03 -07:00
|
|
|
type pp_queue_elem = {
|
2008-01-11 08:13:18 -08:00
|
|
|
mutable elem_size : size;
|
|
|
|
token : pp_token;
|
|
|
|
length : int;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(* Scan stack:
|
1995-05-04 03:15:53 -07:00
|
|
|
each element is (left_total, queue element) where left_total
|
2004-03-05 04:15:31 -08:00
|
|
|
is the value of pp_left_total when the element has been enqueued. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
type pp_scan_elem = Scan_elem of int * pp_queue_elem;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(* Formatting stack:
|
1995-05-04 03:15:53 -07:00
|
|
|
used to break the lines while printing tokens.
|
|
|
|
The formatting stack contains the description of
|
|
|
|
the currently active blocks. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
type pp_format_elem = Format_elem of block_type * int;;
|
1996-08-27 04:57:46 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* General purpose queues, used in the formatter. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
type 'a queue_elem =
|
|
|
|
| Nil
|
|
|
|
| Cons of 'a queue_cell
|
|
|
|
|
|
|
|
and 'a queue_cell = {
|
|
|
|
mutable head : 'a;
|
|
|
|
mutable tail : 'a queue_elem;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-11 14:18:20 -08:00
|
|
|
type 'a queue = {
|
2008-01-11 08:13:18 -08:00
|
|
|
mutable insert : 'a queue_elem;
|
|
|
|
mutable body : 'a queue_elem;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(* The formatter specific tag handling functions. *)
|
2002-03-19 23:33:20 -08:00
|
|
|
type formatter_tag_functions = {
|
2008-01-11 08:13:18 -08:00
|
|
|
mark_open_tag : tag -> string;
|
|
|
|
mark_close_tag : tag -> string;
|
|
|
|
print_open_tag : tag -> unit;
|
|
|
|
print_close_tag : tag -> unit;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
2002-03-19 22:51:17 -08:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(* A formatter with all its machinery. *)
|
2010-04-15 01:39:16 -07:00
|
|
|
type formatter = {
|
2008-01-11 08:13:18 -08:00
|
|
|
mutable pp_scan_stack : pp_scan_elem list;
|
|
|
|
mutable pp_format_stack : pp_format_elem list;
|
|
|
|
mutable pp_tbox_stack : tblock list;
|
|
|
|
mutable pp_tag_stack : tag list;
|
|
|
|
mutable pp_mark_stack : tag list;
|
|
|
|
(* Global variables: default initialization is
|
|
|
|
set_margin 78
|
|
|
|
set_min_space_left 0. *)
|
|
|
|
(* Value of right margin. *)
|
|
|
|
mutable pp_margin : int;
|
|
|
|
(* Minimal space left before margin, when opening a block. *)
|
|
|
|
mutable pp_min_space_left : int;
|
|
|
|
(* Maximum value of indentation:
|
|
|
|
no blocks can be opened further. *)
|
|
|
|
mutable pp_max_indent : int;
|
|
|
|
(* Space remaining on the current line. *)
|
|
|
|
mutable pp_space_left : int;
|
|
|
|
(* Current value of indentation. *)
|
|
|
|
mutable pp_current_indent : int;
|
|
|
|
(* True when the line has been broken by the pretty-printer. *)
|
|
|
|
mutable pp_is_new_line : bool;
|
|
|
|
(* Total width of tokens already printed. *)
|
|
|
|
mutable pp_left_total : int;
|
|
|
|
(* Total width of tokens ever put in queue. *)
|
|
|
|
mutable pp_right_total : int;
|
|
|
|
(* Current number of opened blocks. *)
|
|
|
|
mutable pp_curr_depth : int;
|
|
|
|
(* Maximum number of blocks which can be simultaneously opened. *)
|
|
|
|
mutable pp_max_boxes : int;
|
|
|
|
(* Ellipsis string. *)
|
|
|
|
mutable pp_ellipsis : string;
|
|
|
|
(* Output function. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
mutable pp_out_string : string -> int -> int -> unit;
|
2008-01-11 08:13:18 -08:00
|
|
|
(* Flushing function. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
mutable pp_out_flush : unit -> unit;
|
2008-01-11 08:13:18 -08:00
|
|
|
(* Output of new lines. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
mutable pp_out_newline : unit -> unit;
|
2008-01-11 08:13:18 -08:00
|
|
|
(* Output of indentation spaces. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
mutable pp_out_spaces : int -> unit;
|
2008-01-11 08:13:18 -08:00
|
|
|
(* Are tags printed ? *)
|
|
|
|
mutable pp_print_tags : bool;
|
|
|
|
(* Are tags marked ? *)
|
|
|
|
mutable pp_mark_tags : bool;
|
|
|
|
(* Find opening and closing markers of tags. *)
|
|
|
|
mutable pp_mark_open_tag : tag -> string;
|
|
|
|
mutable pp_mark_close_tag : tag -> string;
|
|
|
|
mutable pp_print_open_tag : tag -> unit;
|
|
|
|
mutable pp_print_close_tag : tag -> unit;
|
|
|
|
(* The pretty-printer queue. *)
|
|
|
|
mutable pp_queue : pp_queue_elem queue;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Auxilliaries and basic functions.
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
|
|
|
|
2002-11-15 02:57:14 -08:00
|
|
|
(* Queues auxilliaries. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
let make_queue () = { insert = Nil; body = Nil; };;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
|
|
|
let clear_queue q = q.insert <- Nil; q.body <- Nil;;
|
|
|
|
|
|
|
|
let add_queue x q =
|
2008-01-11 08:13:18 -08:00
|
|
|
let c = Cons { head = x; tail = Nil; } in
|
|
|
|
match q with
|
2011-06-20 14:46:20 -07:00
|
|
|
| { insert = Cons cell; body = _; } ->
|
2008-01-11 08:13:18 -08:00
|
|
|
q.insert <- c; cell.tail <- c
|
|
|
|
(* Invariant: when insert is Nil body should be Nil. *)
|
2011-06-20 14:46:20 -07:00
|
|
|
| { insert = Nil; body = _; } ->
|
|
|
|
q.insert <- c; q.body <- c
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
|
|
|
exception Empty_queue;;
|
|
|
|
|
|
|
|
let peek_queue = function
|
2011-06-20 14:46:20 -07:00
|
|
|
| { body = Cons { head = x; tail = _; }; _ } -> x
|
|
|
|
| { body = Nil; insert = _; } -> raise Empty_queue
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
|
|
|
let take_queue = function
|
2011-06-20 14:46:20 -07:00
|
|
|
| { body = Cons { head = x; tail = tl; }; _ } as q ->
|
1996-07-08 11:53:26 -07:00
|
|
|
q.body <- tl;
|
2004-03-05 04:15:31 -08:00
|
|
|
if tl = Nil then q.insert <- Nil; (* Maintain the invariant. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
x
|
2011-06-20 14:46:20 -07:00
|
|
|
| { body = Nil; insert = _; } -> raise Empty_queue
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Enter a token in the pretty-printer queue. *)
|
2011-06-20 14:46:20 -07:00
|
|
|
let pp_enqueue state ({ length = len; _} as token) =
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_right_total <- state.pp_right_total + len;
|
2008-06-16 06:04:46 -07:00
|
|
|
add_queue token state.pp_queue
|
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
|
|
|
let pp_clear_queue state =
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_left_total <- 1; state.pp_right_total <- 1;
|
2008-06-16 06:04:46 -07:00
|
|
|
clear_queue state.pp_queue
|
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
2004-07-13 05:25:21 -07:00
|
|
|
(* Pp_infinity: large value for default tokens size.
|
|
|
|
|
|
|
|
Pp_infinity is documented as being greater than 1e10; to avoid
|
2005-09-20 01:41:09 -07:00
|
|
|
confusion about the word ``greater'', we choose pp_infinity greater
|
|
|
|
than 1e10 + 1; for correct handling of tests in the algorithm,
|
|
|
|
pp_infinity must be even one more than 1e10 + 1; let's stand on the
|
2004-07-13 05:25:21 -07:00
|
|
|
safe side by choosing 1.e10+10.
|
|
|
|
|
|
|
|
Pp_infinity could probably be 1073741823 that is 2^30 - 1, that is
|
2005-09-20 01:41:09 -07:00
|
|
|
the minimal upper bound for integers; now that max_int is defined,
|
|
|
|
this limit could also be defined as max_int - 1.
|
|
|
|
|
|
|
|
However, before setting pp_infinity to something around max_int, we
|
|
|
|
must carefully double-check all the integer arithmetic operations
|
|
|
|
that involve pp_infinity, since any overflow would wreck havoc the
|
|
|
|
pretty-printing algorithm's invariants. Given that this arithmetic
|
|
|
|
correctness check is difficult and error prone and given that 1e10
|
|
|
|
+ 1 is in practice large enough, there is no need to attempt to set
|
2007-05-08 14:30:01 -07:00
|
|
|
pp_infinity to the theoretically maximum limit. It is not worth the
|
2005-09-20 01:41:09 -07:00
|
|
|
burden ! *)
|
2004-07-13 05:25:21 -07:00
|
|
|
|
|
|
|
let pp_infinity = 1000000010;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Output functions for the formatter. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
let pp_output_string state s = state.pp_out_string s 0 (String.length s)
|
|
|
|
and pp_output_newline state = state.pp_out_newline ()
|
|
|
|
and pp_output_spaces state n = state.pp_out_spaces n
|
2008-01-11 08:13:18 -08:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a break, indenting a new line. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let break_new_line state offset width =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_output_newline state;
|
|
|
|
state.pp_is_new_line <- true;
|
|
|
|
let indent = state.pp_margin - width + offset in
|
|
|
|
(* Don't indent more than pp_max_indent. *)
|
|
|
|
let real_indent = min state.pp_max_indent indent in
|
|
|
|
state.pp_current_indent <- real_indent;
|
|
|
|
state.pp_space_left <- state.pp_margin - state.pp_current_indent;
|
2012-04-27 02:56:05 -07:00
|
|
|
pp_output_spaces state state.pp_current_indent
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To force a line break inside a block: no offset is added. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let break_line state width = break_new_line state 0 width;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a break that fits on the current line. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let break_same_line state width =
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_space_left <- state.pp_space_left - width;
|
2012-04-27 02:56:05 -07:00
|
|
|
pp_output_spaces state width
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* To indent no more than pp_max_indent, if one tries to open a block
|
|
|
|
beyond pp_max_indent, then the block is rejected on the left
|
|
|
|
by simulating a break. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_force_break_line state =
|
2008-01-11 08:13:18 -08:00
|
|
|
match state.pp_format_stack with
|
|
|
|
| Format_elem (bl_ty, width) :: _ ->
|
|
|
|
if width > state.pp_space_left then
|
|
|
|
(match bl_ty with
|
|
|
|
| Pp_fits -> () | Pp_hbox -> ()
|
2011-06-20 14:46:20 -07:00
|
|
|
| Pp_vbox | Pp_hvbox | Pp_hovbox | Pp_box ->
|
|
|
|
break_line state width)
|
|
|
|
| [] -> pp_output_newline state
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To skip a token, if the previous line has been broken. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_skip_token state =
|
2008-01-11 08:13:18 -08:00
|
|
|
(* When calling pp_skip_token the queue cannot be empty. *)
|
|
|
|
match take_queue state.pp_queue with
|
2011-06-20 14:46:20 -07:00
|
|
|
| { elem_size = size; length = len; token = _; } ->
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_left_total <- state.pp_left_total - len;
|
2008-06-16 06:04:46 -07:00
|
|
|
state.pp_space_left <- state.pp_space_left + int_of_size size
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(**************************************************************
|
|
|
|
|
2007-05-08 14:30:01 -07:00
|
|
|
The main pretty printing functions.
|
2002-03-05 12:56:46 -08:00
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a token. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let format_pp_token state size = function
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-08-27 04:57:46 -07:00
|
|
|
| Pp_text s ->
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_space_left <- state.pp_space_left - size;
|
|
|
|
pp_output_string state s;
|
|
|
|
state.pp_is_new_line <- false
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1997-10-23 00:53:12 -07:00
|
|
|
| Pp_begin (off, ty) ->
|
2008-01-11 08:13:18 -08:00
|
|
|
let insertion_point = state.pp_margin - state.pp_space_left in
|
|
|
|
if insertion_point > state.pp_max_indent then
|
|
|
|
(* can't open a block right there. *)
|
|
|
|
begin pp_force_break_line state end;
|
|
|
|
let offset = state.pp_space_left - off in
|
|
|
|
let bl_type =
|
|
|
|
begin match ty with
|
|
|
|
| Pp_vbox -> Pp_vbox
|
2011-06-20 14:46:20 -07:00
|
|
|
| Pp_hbox | Pp_hvbox | Pp_hovbox | Pp_box | Pp_fits ->
|
|
|
|
if size > state.pp_space_left then ty else Pp_fits
|
2008-01-11 08:13:18 -08:00
|
|
|
end in
|
|
|
|
state.pp_format_stack <-
|
|
|
|
Format_elem (bl_type, offset) :: state.pp_format_stack
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
| Pp_end ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_format_stack with
|
2011-06-20 14:46:20 -07:00
|
|
|
| _ :: ls -> state.pp_format_stack <- ls
|
|
|
|
| [] -> () (* No more block to close. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_tbegin (Pp_tbox _ as tbox) ->
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_tbox_stack <- tbox :: state.pp_tbox_stack
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
| Pp_tend ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_tbox_stack with
|
2011-06-20 14:46:20 -07:00
|
|
|
| _ :: ls -> state.pp_tbox_stack <- ls
|
|
|
|
| [] -> () (* No more tabulation block to close. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
| Pp_stab ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_tbox_stack with
|
|
|
|
| Pp_tbox tabs :: _ ->
|
|
|
|
let rec add_tab n = function
|
|
|
|
| [] -> [n]
|
|
|
|
| x :: l as ls -> if n < x then n :: ls else x :: add_tab n l in
|
|
|
|
tabs := add_tab (state.pp_margin - state.pp_space_left) !tabs
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> () (* No opened tabulation block. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_tbreak (n, off) ->
|
2008-01-11 08:13:18 -08:00
|
|
|
let insertion_point = state.pp_margin - state.pp_space_left in
|
|
|
|
begin match state.pp_tbox_stack with
|
|
|
|
| Pp_tbox tabs :: _ ->
|
|
|
|
let rec find n = function
|
|
|
|
| x :: l -> if x >= n then x else find n l
|
|
|
|
| [] -> raise Not_found in
|
|
|
|
let tab =
|
|
|
|
match !tabs with
|
2011-06-20 14:46:20 -07:00
|
|
|
| x :: _ ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin
|
|
|
|
try find insertion_point !tabs with
|
|
|
|
| Not_found -> x
|
|
|
|
end
|
|
|
|
| _ -> insertion_point in
|
|
|
|
let offset = tab - insertion_point in
|
|
|
|
if offset >= 0
|
|
|
|
then break_same_line state (offset + n)
|
|
|
|
else break_new_line state (tab + off) state.pp_margin
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> () (* No opened tabulation block. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
| Pp_newline ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_format_stack with
|
|
|
|
| Format_elem (_, width) :: _ -> break_line state width
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> pp_output_newline state (* No opened block. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
| Pp_if_newline ->
|
2008-01-11 08:13:18 -08:00
|
|
|
if state.pp_current_indent != state.pp_margin - state.pp_space_left
|
|
|
|
then pp_skip_token state
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
| Pp_break (n, off) ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_format_stack with
|
|
|
|
| Format_elem (ty, width) :: _ ->
|
|
|
|
begin match ty with
|
|
|
|
| Pp_hovbox ->
|
|
|
|
if size > state.pp_space_left
|
|
|
|
then break_new_line state off width
|
|
|
|
else break_same_line state n
|
|
|
|
| Pp_box ->
|
|
|
|
(* Have the line just been broken here ? *)
|
|
|
|
if state.pp_is_new_line then break_same_line state n else
|
|
|
|
if size > state.pp_space_left
|
|
|
|
then break_new_line state off width else
|
|
|
|
(* break the line here leads to new indentation ? *)
|
|
|
|
if state.pp_current_indent > state.pp_margin - width + off
|
|
|
|
then break_new_line state off width
|
|
|
|
else break_same_line state n
|
|
|
|
| Pp_hvbox -> break_new_line state off width
|
|
|
|
| Pp_fits -> break_same_line state n
|
|
|
|
| Pp_vbox -> break_new_line state off width
|
|
|
|
| Pp_hbox -> break_same_line state n
|
|
|
|
end
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> () (* No opened block. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
| Pp_open_tag tag_name ->
|
2008-01-11 08:13:18 -08:00
|
|
|
let marker = state.pp_mark_open_tag tag_name in
|
|
|
|
pp_output_string state marker;
|
|
|
|
state.pp_mark_stack <- tag_name :: state.pp_mark_stack
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
| Pp_close_tag ->
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match state.pp_mark_stack with
|
|
|
|
| tag_name :: tags ->
|
|
|
|
let marker = state.pp_mark_close_tag tag_name in
|
|
|
|
pp_output_string state marker;
|
|
|
|
state.pp_mark_stack <- tags
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> () (* No more tag to close. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Print if token size is known or printing is delayed.
|
|
|
|
Size is known when not negative.
|
1995-05-04 03:15:53 -07:00
|
|
|
Printing is delayed when the text waiting in the queue requires
|
2008-09-08 05:30:19 -07:00
|
|
|
more room to format than exists on the current line.
|
|
|
|
|
|
|
|
Note: [advance_loop] must be tail recursive to prevent stack overflows. *)
|
2007-05-08 14:30:01 -07:00
|
|
|
let rec advance_loop state =
|
|
|
|
match peek_queue state.pp_queue with
|
|
|
|
| {elem_size = size; token = tok; length = len} ->
|
|
|
|
let size = int_of_size size in
|
|
|
|
if not
|
|
|
|
(size < 0 &&
|
|
|
|
(state.pp_right_total - state.pp_left_total < state.pp_space_left))
|
|
|
|
then begin
|
2008-06-16 06:04:46 -07:00
|
|
|
ignore (take_queue state.pp_queue);
|
2007-05-08 14:30:01 -07:00
|
|
|
format_pp_token state (if size < 0 then pp_infinity else size) tok;
|
|
|
|
state.pp_left_total <- len + state.pp_left_total;
|
|
|
|
advance_loop state
|
2008-06-16 06:04:46 -07:00
|
|
|
end
|
|
|
|
;;
|
2007-05-08 14:30:01 -07:00
|
|
|
|
|
|
|
let advance_left state =
|
|
|
|
try advance_loop state with
|
2008-06-16 06:04:46 -07:00
|
|
|
| Empty_queue -> ()
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let enqueue_advance state tok = pp_enqueue state tok; advance_left state;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To enqueue a string : try to advance. *)
|
2005-09-20 10:18:03 -07:00
|
|
|
let make_queue_elem size tok len =
|
2008-01-11 08:13:18 -08:00
|
|
|
{ elem_size = size; token = tok; length = len; };;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
let enqueue_string_as state size s =
|
|
|
|
let len = int_of_size size in
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_advance state (make_queue_elem size (Pp_text s) len)
|
|
|
|
;;
|
2005-09-20 10:18:03 -07:00
|
|
|
|
|
|
|
let enqueue_string state s =
|
|
|
|
let len = String.length s in
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_string_as state (size_of_int len) s
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* Routines for scan stack
|
2004-03-05 04:15:31 -08:00
|
|
|
determine sizes of blocks. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* The scan_stack is never empty. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let scan_stack_bottom =
|
2005-09-20 10:18:03 -07:00
|
|
|
let q_elem = make_queue_elem (size_of_int (-1)) (Pp_text "") 0 in
|
2008-06-16 06:04:46 -07:00
|
|
|
[Scan_elem (-1, q_elem)]
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* Set size of blocks on scan stack:
|
2004-03-05 04:15:31 -08:00
|
|
|
if ty = true then size of break is set else size of block is set;
|
|
|
|
in each case pp_scan_stack is popped. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let clear_scan_stack state = state.pp_scan_stack <- scan_stack_bottom;;
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
(* Pattern matching on scan stack is exhaustive,
|
|
|
|
since scan_stack is never empty.
|
|
|
|
Pattern matching on token in scan stack is also exhaustive,
|
2004-03-05 04:15:31 -08:00
|
|
|
since scan_push is used on breaks and opening of boxes. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let set_size state ty =
|
2008-01-11 08:13:18 -08:00
|
|
|
match state.pp_scan_stack with
|
|
|
|
| Scan_elem
|
|
|
|
(left_tot,
|
2011-06-20 14:46:20 -07:00
|
|
|
({ elem_size = size; token = tok; length = _; } as queue_elem)) :: t ->
|
2008-01-11 08:13:18 -08:00
|
|
|
let size = int_of_size size in
|
|
|
|
(* test if scan stack contains any data that is not obsolete. *)
|
|
|
|
if left_tot < state.pp_left_total then clear_scan_stack state else
|
|
|
|
begin match tok with
|
|
|
|
| Pp_break (_, _) | Pp_tbreak (_, _) ->
|
|
|
|
if ty then
|
|
|
|
begin
|
|
|
|
queue_elem.elem_size <- size_of_int (state.pp_right_total + size);
|
|
|
|
state.pp_scan_stack <- t
|
|
|
|
end
|
|
|
|
| Pp_begin (_, _) ->
|
|
|
|
if not ty then
|
|
|
|
begin
|
|
|
|
queue_elem.elem_size <- size_of_int (state.pp_right_total + size);
|
|
|
|
state.pp_scan_stack <- t
|
1995-05-04 03:15:53 -07:00
|
|
|
end
|
2011-06-20 14:46:20 -07:00
|
|
|
| Pp_text _ | Pp_stab | Pp_tbegin _ | Pp_tend | Pp_end
|
|
|
|
| Pp_newline | Pp_if_newline
|
|
|
|
| Pp_open_tag _ | Pp_close_tag ->
|
|
|
|
() (* scan_push is only used for breaks and boxes. *)
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
2011-06-20 14:46:20 -07:00
|
|
|
| [] -> () (* scan_stack is never empty. *)
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Push a token on scan stack. If b is true set_size is called. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let scan_push state b tok =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_enqueue state tok;
|
|
|
|
if b then set_size state true;
|
|
|
|
state.pp_scan_stack <-
|
2008-06-16 06:04:46 -07:00
|
|
|
Scan_elem (state.pp_right_total, tok) :: state.pp_scan_stack
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-11-04 13:43:01 -08:00
|
|
|
(* To open a new block :
|
|
|
|
the user may set the depth bound pp_max_boxes
|
2004-03-05 04:15:31 -08:00
|
|
|
any text nested deeper is printed as the ellipsis string. *)
|
1997-09-05 11:26:53 -07:00
|
|
|
let pp_open_box_gen state indent br_ty =
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_curr_depth <- state.pp_curr_depth + 1;
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
|
|
|
let elem =
|
|
|
|
make_queue_elem
|
|
|
|
(size_of_int (- state.pp_right_total))
|
|
|
|
(Pp_begin (indent, br_ty))
|
|
|
|
0 in
|
|
|
|
scan_push state false elem else
|
|
|
|
if state.pp_curr_depth = state.pp_max_boxes
|
2008-06-16 06:04:46 -07:00
|
|
|
then enqueue_string state state.pp_ellipsis
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* The box which is always opened. *)
|
2004-03-07 23:16:37 -08:00
|
|
|
let pp_open_sys_box state = pp_open_box_gen state 0 Pp_hovbox;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2007-05-08 14:30:01 -07:00
|
|
|
(* Close a block, setting sizes of its sub blocks. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_close_box state () =
|
2008-01-11 08:13:18 -08:00
|
|
|
if state.pp_curr_depth > 1 then
|
|
|
|
begin
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
|
|
|
begin
|
|
|
|
pp_enqueue state
|
|
|
|
{ elem_size = size_of_int 0; token = Pp_end; length = 0; };
|
|
|
|
set_size state true; set_size state false
|
|
|
|
end;
|
|
|
|
state.pp_curr_depth <- state.pp_curr_depth - 1;
|
2008-06-16 06:04:46 -07:00
|
|
|
end
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-03-11 14:18:20 -08:00
|
|
|
(* Open a tag, pushing it on the tag stack. *)
|
2002-03-19 23:33:20 -08:00
|
|
|
let pp_open_tag state tag_name =
|
2008-01-11 08:13:18 -08:00
|
|
|
if state.pp_print_tags then
|
|
|
|
begin
|
|
|
|
state.pp_tag_stack <- tag_name :: state.pp_tag_stack;
|
|
|
|
state.pp_print_open_tag tag_name
|
|
|
|
end;
|
|
|
|
if state.pp_mark_tags then
|
|
|
|
pp_enqueue state {
|
|
|
|
elem_size = size_of_int 0;
|
|
|
|
token = Pp_open_tag tag_name;
|
|
|
|
length = 0;
|
|
|
|
}
|
|
|
|
;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
(* Close a tag, popping it from the tag stack. *)
|
|
|
|
let pp_close_tag state () =
|
2008-01-11 08:13:18 -08:00
|
|
|
if state.pp_mark_tags then
|
|
|
|
pp_enqueue state {
|
|
|
|
elem_size = size_of_int 0;
|
|
|
|
token = Pp_close_tag;
|
|
|
|
length = 0;
|
|
|
|
};
|
|
|
|
if state.pp_print_tags then
|
|
|
|
begin
|
|
|
|
match state.pp_tag_stack with
|
|
|
|
| tag_name :: tags ->
|
|
|
|
state.pp_print_close_tag tag_name;
|
|
|
|
state.pp_tag_stack <- tags
|
|
|
|
| _ -> () (* No more tag to close. *)
|
2008-06-16 06:04:46 -07:00
|
|
|
end
|
|
|
|
;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
let pp_set_print_tags state b = state.pp_print_tags <- b;;
|
2002-03-19 23:33:20 -08:00
|
|
|
let pp_set_mark_tags state b = state.pp_mark_tags <- b;;
|
2002-03-22 12:43:07 -08:00
|
|
|
let pp_get_print_tags state () = state.pp_print_tags;;
|
|
|
|
let pp_get_mark_tags state () = state.pp_mark_tags;;
|
2002-05-08 06:50:29 -07:00
|
|
|
let pp_set_tags state b = pp_set_print_tags state b; pp_set_mark_tags state b;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
let pp_get_formatter_tag_functions state () = {
|
2008-01-11 08:13:18 -08:00
|
|
|
mark_open_tag = state.pp_mark_open_tag;
|
|
|
|
mark_close_tag = state.pp_mark_close_tag;
|
|
|
|
print_open_tag = state.pp_print_open_tag;
|
|
|
|
print_close_tag = state.pp_print_close_tag;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2004-02-11 14:20:04 -08:00
|
|
|
let pp_set_formatter_tag_functions state {
|
|
|
|
mark_open_tag = mot;
|
|
|
|
mark_close_tag = mct;
|
|
|
|
print_open_tag = pot;
|
|
|
|
print_close_tag = pct;
|
|
|
|
} =
|
|
|
|
state.pp_mark_open_tag <- mot;
|
|
|
|
state.pp_mark_close_tag <- mct;
|
|
|
|
state.pp_print_open_tag <- pot;
|
2008-06-16 06:04:46 -07:00
|
|
|
state.pp_print_close_tag <- pct
|
|
|
|
;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
(* Initialize pretty-printer. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_rinit state =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_clear_queue state;
|
|
|
|
clear_scan_stack state;
|
|
|
|
state.pp_format_stack <- [];
|
|
|
|
state.pp_tbox_stack <- [];
|
|
|
|
state.pp_tag_stack <- [];
|
|
|
|
state.pp_mark_stack <- [];
|
|
|
|
state.pp_current_indent <- 0;
|
|
|
|
state.pp_curr_depth <- 0;
|
|
|
|
state.pp_space_left <- state.pp_margin;
|
|
|
|
pp_open_sys_box state;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* Flushing pretty-printer queue. *)
|
1999-02-16 01:07:26 -08:00
|
|
|
let pp_flush_queue state b =
|
2008-01-11 08:13:18 -08:00
|
|
|
while state.pp_curr_depth > 1 do
|
|
|
|
pp_close_box state ()
|
|
|
|
done;
|
|
|
|
state.pp_right_total <- pp_infinity;
|
|
|
|
advance_left state;
|
|
|
|
if b then pp_output_newline state;
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_rinit state
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Procedures to format objects, and use boxes
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a string. *)
|
2005-09-20 10:18:03 -07:00
|
|
|
let pp_print_as_size state size s =
|
1996-07-08 11:53:26 -07:00
|
|
|
if state.pp_curr_depth < state.pp_max_boxes
|
2008-06-16 06:04:46 -07:00
|
|
|
then enqueue_string_as state size s
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
let pp_print_as state isize s =
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_print_as_size state (size_of_int isize) s
|
|
|
|
;;
|
2005-09-20 10:18:03 -07:00
|
|
|
|
|
|
|
let pp_print_string state s =
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_print_as state (String.length s) s
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format an integer. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_int state i = pp_print_string state (string_of_int i);;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a float. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_float state f = pp_print_string state (string_of_float f);;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a boolean. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_bool state b = pp_print_string state (string_of_bool b);;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format a char. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_char state c =
|
2005-09-20 10:18:03 -07:00
|
|
|
let s = String.create 1 in
|
|
|
|
s.[0] <- c;
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_print_as state 1 s
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Opening boxes. *)
|
1997-09-05 11:26:53 -07:00
|
|
|
let pp_open_hbox state () = pp_open_box_gen state 0 Pp_hbox
|
|
|
|
and pp_open_vbox state indent = pp_open_box_gen state indent Pp_vbox
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1997-09-05 11:26:53 -07:00
|
|
|
and pp_open_hvbox state indent = pp_open_box_gen state indent Pp_hvbox
|
|
|
|
and pp_open_hovbox state indent = pp_open_box_gen state indent Pp_hovbox
|
|
|
|
and pp_open_box state indent = pp_open_box_gen state indent Pp_box;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* Print a new line after printing all queued text
|
2004-03-05 04:15:31 -08:00
|
|
|
(same for print_flush but without a newline). *)
|
1999-02-16 01:07:26 -08:00
|
|
|
let pp_print_newline state () =
|
2012-04-27 02:56:05 -07:00
|
|
|
pp_flush_queue state true; state.pp_out_flush ()
|
1999-02-16 01:07:26 -08:00
|
|
|
and pp_print_flush state () =
|
2012-04-27 02:56:05 -07:00
|
|
|
pp_flush_queue state false; state.pp_out_flush ();;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To get a newline when one does not want to close the current block. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_force_newline state () =
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_newline 0)
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To format something if the line has just been broken. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_if_newline state () =
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_if_newline 0)
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* Breaks: indicate where a block may be broken.
|
|
|
|
If line is broken then offset is added to the indentation of the current
|
1996-07-08 11:53:26 -07:00
|
|
|
block else (the value of) width blanks are printed.
|
2004-03-05 04:15:31 -08:00
|
|
|
To do (?) : add a maximum width and offset value. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_break state width offset =
|
2002-03-05 12:56:46 -08:00
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2005-09-20 10:18:03 -07:00
|
|
|
let elem =
|
|
|
|
make_queue_elem
|
|
|
|
(size_of_int (- state.pp_right_total))
|
|
|
|
(Pp_break (width, offset))
|
|
|
|
width in
|
2008-06-16 06:04:46 -07:00
|
|
|
scan_push state true elem
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
|
|
|
let pp_print_space state () = pp_print_break state 1 0
|
2008-06-16 06:04:46 -07:00
|
|
|
and pp_print_cut state () = pp_print_break state 0 0
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Tabulation boxes. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_open_tbox state () =
|
|
|
|
state.pp_curr_depth <- state.pp_curr_depth + 1;
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2005-09-20 10:18:03 -07:00
|
|
|
let elem =
|
|
|
|
make_queue_elem (size_of_int 0) (Pp_tbegin (Pp_tbox (ref []))) 0 in
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_advance state elem
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Close a tabulation block. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_close_tbox state () =
|
2008-01-11 08:13:18 -08:00
|
|
|
if state.pp_curr_depth > 1 then
|
|
|
|
begin
|
1996-08-27 04:57:46 -07:00
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2005-09-20 10:18:03 -07:00
|
|
|
let elem = make_queue_elem (size_of_int 0) Pp_tend 0 in
|
|
|
|
enqueue_advance state elem;
|
2008-01-11 08:13:18 -08:00
|
|
|
state.pp_curr_depth <- state.pp_curr_depth - 1
|
2008-06-16 06:04:46 -07:00
|
|
|
end
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Print a tabulation break. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_tbreak state width offset =
|
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
2005-09-20 10:18:03 -07:00
|
|
|
let elem =
|
|
|
|
make_queue_elem
|
|
|
|
(size_of_int (- state.pp_right_total))
|
|
|
|
(Pp_tbreak (width, offset))
|
|
|
|
width in
|
2008-06-16 06:04:46 -07:00
|
|
|
scan_push state true elem
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_print_tab state () = pp_print_tbreak state 0 0;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_tab state () =
|
2005-09-20 10:18:03 -07:00
|
|
|
if state.pp_curr_depth < state.pp_max_boxes then
|
|
|
|
let elem =
|
|
|
|
make_queue_elem (size_of_int 0) Pp_stab 0 in
|
2008-06-16 06:04:46 -07:00
|
|
|
enqueue_advance state elem
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(**************************************************************
|
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
Procedures to control the pretty-printers
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Fit max_boxes. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_max_boxes state n = if n > 1 then state.pp_max_boxes <- n;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To know the current maximum number of boxes allowed. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_get_max_boxes state () = state.pp_max_boxes;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1997-09-16 06:46:36 -07:00
|
|
|
let pp_over_max_boxes state () = state.pp_curr_depth = state.pp_max_boxes;;
|
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* Ellipsis. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_ellipsis_text state s = state.pp_ellipsis <- s
|
2008-06-16 06:04:46 -07:00
|
|
|
and pp_get_ellipsis_text state () = state.pp_ellipsis
|
|
|
|
;;
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-03-05 04:15:31 -08:00
|
|
|
(* To set the margin of pretty-printer. *)
|
2004-07-13 05:25:21 -07:00
|
|
|
let pp_limit n =
|
2008-06-16 06:04:46 -07:00
|
|
|
if n < pp_infinity then n else pred pp_infinity
|
|
|
|
;;
|
2004-07-13 05:25:21 -07:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_min_space_left state n =
|
2004-07-13 05:25:21 -07:00
|
|
|
if n >= 1 then
|
|
|
|
let n = pp_limit n in
|
1996-07-08 11:53:26 -07:00
|
|
|
state.pp_min_space_left <- n;
|
|
|
|
state.pp_max_indent <- state.pp_margin - state.pp_min_space_left;
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_rinit state
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-19 22:51:17 -08:00
|
|
|
(* Initially, we have :
|
1996-07-08 11:53:26 -07:00
|
|
|
pp_max_indent = pp_margin - pp_min_space_left, and
|
2004-03-05 04:15:31 -08:00
|
|
|
pp_space_left = pp_margin. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_max_indent state n =
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_set_min_space_left state (state.pp_margin - n)
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_get_max_indent state () = state.pp_max_indent;;
|
|
|
|
|
|
|
|
let pp_set_margin state n =
|
2004-07-13 05:25:21 -07:00
|
|
|
if n >= 1 then
|
|
|
|
let n = pp_limit n in
|
1996-07-08 11:53:26 -07:00
|
|
|
state.pp_margin <- n;
|
|
|
|
let new_max_indent =
|
2008-01-11 08:13:18 -08:00
|
|
|
(* Try to maintain max_indent to its actual value. *)
|
|
|
|
if state.pp_max_indent <= state.pp_margin
|
|
|
|
then state.pp_max_indent else
|
|
|
|
(* If possible maintain pp_min_space_left to its actual value,
|
|
|
|
if this leads to a too small max_indent, take half of the
|
|
|
|
new margin, if it is greater than 1. *)
|
|
|
|
max (max (state.pp_margin - state.pp_min_space_left)
|
|
|
|
(state.pp_margin / 2)) 1 in
|
2008-11-08 06:58:40 -08:00
|
|
|
(* Rebuild invariants. *)
|
2008-06-16 06:04:46 -07:00
|
|
|
pp_set_max_indent state new_max_indent
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
|
|
|
let pp_get_margin state () = state.pp_margin;;
|
|
|
|
|
2012-04-27 02:56:05 -07:00
|
|
|
type formatter_out_functions = {
|
|
|
|
out_string : string -> int -> int -> unit;
|
|
|
|
out_flush : unit -> unit;
|
|
|
|
out_newline : unit -> unit;
|
|
|
|
out_spaces : int -> unit;
|
|
|
|
}
|
|
|
|
;;
|
|
|
|
|
|
|
|
let pp_set_formatter_out_functions state {
|
|
|
|
out_string = f;
|
|
|
|
out_flush = g;
|
|
|
|
out_newline = h;
|
|
|
|
out_spaces = i;
|
|
|
|
} =
|
|
|
|
state.pp_out_string <- f;
|
|
|
|
state.pp_out_flush <- g;
|
|
|
|
state.pp_out_newline <- h;
|
|
|
|
state.pp_out_spaces <- i;
|
|
|
|
;;
|
|
|
|
|
|
|
|
let pp_get_formatter_out_functions state () = {
|
|
|
|
out_string = state.pp_out_string;
|
|
|
|
out_flush = state.pp_out_flush;
|
|
|
|
out_newline = state.pp_out_newline;
|
|
|
|
out_spaces = state.pp_out_spaces;
|
|
|
|
}
|
|
|
|
;;
|
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let pp_set_formatter_output_functions state f g =
|
2012-04-27 02:56:05 -07:00
|
|
|
state.pp_out_string <- f; state.pp_out_flush <- g;;
|
2002-03-05 12:56:46 -08:00
|
|
|
let pp_get_formatter_output_functions state () =
|
2012-04-27 02:56:05 -07:00
|
|
|
(state.pp_out_string, state.pp_out_flush)
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2001-09-06 01:52:32 -07:00
|
|
|
let pp_set_all_formatter_output_functions state
|
|
|
|
~out:f ~flush:g ~newline:h ~spaces:i =
|
1998-12-02 02:15:37 -08:00
|
|
|
pp_set_formatter_output_functions state f g;
|
2012-04-27 02:56:05 -07:00
|
|
|
state.pp_out_newline <- h;
|
|
|
|
state.pp_out_spaces <- i;
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
2002-03-05 12:56:46 -08:00
|
|
|
let pp_get_all_formatter_output_functions state () =
|
2012-04-27 02:56:05 -07:00
|
|
|
(state.pp_out_string, state.pp_out_flush,
|
|
|
|
state.pp_out_newline, state.pp_out_spaces)
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
2010-05-03 00:09:33 -07:00
|
|
|
(* Default function to output new lines. *)
|
2012-04-27 02:56:05 -07:00
|
|
|
let display_newline state () = state.pp_out_string "\n" 0 1;;
|
2010-05-03 00:09:33 -07:00
|
|
|
|
|
|
|
(* Default function to output spaces. *)
|
|
|
|
let blank_line = String.make 80 ' ';;
|
|
|
|
let rec display_blanks state n =
|
|
|
|
if n > 0 then
|
2012-04-27 02:56:05 -07:00
|
|
|
if n <= 80 then state.pp_out_string blank_line 0 n else
|
2010-05-03 00:09:33 -07:00
|
|
|
begin
|
2012-04-27 02:56:05 -07:00
|
|
|
state.pp_out_string blank_line 0 80;
|
2010-05-03 00:09:33 -07:00
|
|
|
display_blanks state (n - 80)
|
|
|
|
end
|
|
|
|
;;
|
|
|
|
|
1998-12-02 02:15:37 -08:00
|
|
|
let pp_set_formatter_out_channel state os =
|
2012-04-27 02:56:05 -07:00
|
|
|
state.pp_out_string <- output os;
|
|
|
|
state.pp_out_flush <- (fun () -> flush os);
|
|
|
|
state.pp_out_newline <- display_newline state;
|
|
|
|
state.pp_out_spaces <- display_blanks state;
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Creation of specific formatters
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2002-03-19 23:33:20 -08:00
|
|
|
let default_pp_mark_open_tag s = "<" ^ s ^ ">";;
|
|
|
|
let default_pp_mark_close_tag s = "</" ^ s ^ ">";;
|
|
|
|
|
2012-04-27 02:56:05 -07:00
|
|
|
let default_pp_print_open_tag = ignore;;
|
|
|
|
let default_pp_print_close_tag = ignore;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
let pp_make_formatter f g h i =
|
2008-01-11 08:13:18 -08:00
|
|
|
(* The initial state of the formatter contains a dummy box. *)
|
|
|
|
let pp_q = make_queue () in
|
|
|
|
let sys_tok =
|
|
|
|
make_queue_elem (size_of_int (-1)) (Pp_begin (0, Pp_hovbox)) 0 in
|
|
|
|
add_queue sys_tok pp_q;
|
|
|
|
let sys_scan_stack =
|
|
|
|
(Scan_elem (1, sys_tok)) :: scan_stack_bottom in
|
2008-11-08 06:58:40 -08:00
|
|
|
{
|
|
|
|
pp_scan_stack = sys_scan_stack;
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_format_stack = [];
|
|
|
|
pp_tbox_stack = [];
|
|
|
|
pp_tag_stack = [];
|
|
|
|
pp_mark_stack = [];
|
|
|
|
pp_margin = 78;
|
|
|
|
pp_min_space_left = 10;
|
|
|
|
pp_max_indent = 78 - 10;
|
|
|
|
pp_space_left = 78;
|
|
|
|
pp_current_indent = 0;
|
|
|
|
pp_is_new_line = true;
|
|
|
|
pp_left_total = 1;
|
|
|
|
pp_right_total = 1;
|
|
|
|
pp_curr_depth = 1;
|
|
|
|
pp_max_boxes = max_int;
|
|
|
|
pp_ellipsis = ".";
|
2012-04-27 02:56:05 -07:00
|
|
|
pp_out_string = f;
|
|
|
|
pp_out_flush = g;
|
|
|
|
pp_out_newline = h;
|
|
|
|
pp_out_spaces = i;
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_print_tags = false;
|
|
|
|
pp_mark_tags = false;
|
|
|
|
pp_mark_open_tag = default_pp_mark_open_tag;
|
|
|
|
pp_mark_close_tag = default_pp_mark_close_tag;
|
|
|
|
pp_print_open_tag = default_pp_print_open_tag;
|
|
|
|
pp_print_close_tag = default_pp_print_close_tag;
|
|
|
|
pp_queue = pp_q;
|
2008-06-16 06:04:46 -07:00
|
|
|
}
|
|
|
|
;;
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2007-05-08 14:30:01 -07:00
|
|
|
(* Make a formatter with default functions to output spaces and new lines. *)
|
|
|
|
let make_formatter output flush =
|
2008-06-16 06:04:46 -07:00
|
|
|
let ppf = pp_make_formatter output flush ignore ignore in
|
2012-04-27 02:56:05 -07:00
|
|
|
ppf.pp_out_newline <- display_newline ppf;
|
|
|
|
ppf.pp_out_spaces <- display_blanks ppf;
|
2008-06-16 06:04:46 -07:00
|
|
|
ppf
|
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1998-12-08 00:29:54 -08:00
|
|
|
let formatter_of_out_channel oc =
|
2008-06-16 06:04:46 -07:00
|
|
|
make_formatter (output oc) (fun () -> flush oc)
|
|
|
|
;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1999-02-16 01:07:26 -08:00
|
|
|
let formatter_of_buffer b =
|
2008-06-16 06:04:46 -07:00
|
|
|
make_formatter (Buffer.add_substring b) ignore
|
|
|
|
;;
|
1999-02-16 01:07:26 -08:00
|
|
|
|
1999-02-23 10:01:17 -08:00
|
|
|
let stdbuf = Buffer.create 512;;
|
1998-12-02 02:15:37 -08:00
|
|
|
|
2007-05-08 14:30:01 -07:00
|
|
|
(* Predefined formatters. *)
|
2010-04-15 01:39:16 -07:00
|
|
|
let std_formatter = formatter_of_out_channel Pervasives.stdout
|
|
|
|
and err_formatter = formatter_of_out_channel Pervasives.stderr
|
|
|
|
and str_formatter = formatter_of_buffer stdbuf
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1997-05-15 03:41:17 -07:00
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
let flush_str_formatter () =
|
|
|
|
pp_flush_queue str_formatter false;
|
2002-03-19 22:51:17 -08:00
|
|
|
let s = Buffer.contents stdbuf in
|
|
|
|
Buffer.reset stdbuf;
|
2008-06-16 06:04:46 -07:00
|
|
|
s
|
|
|
|
;;
|
1999-02-23 10:01:17 -08:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Basic functions on the standard formatter
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
let open_hbox = pp_open_hbox std_formatter
|
|
|
|
and open_vbox = pp_open_vbox std_formatter
|
|
|
|
and open_hvbox = pp_open_hvbox std_formatter
|
|
|
|
and open_hovbox = pp_open_hovbox std_formatter
|
|
|
|
and open_box = pp_open_box std_formatter
|
|
|
|
and close_box = pp_close_box std_formatter
|
2002-03-11 14:18:20 -08:00
|
|
|
and open_tag = pp_open_tag std_formatter
|
|
|
|
and close_tag = pp_close_tag std_formatter
|
1996-07-08 11:53:26 -07:00
|
|
|
and print_as = pp_print_as std_formatter
|
|
|
|
and print_string = pp_print_string std_formatter
|
|
|
|
and print_int = pp_print_int std_formatter
|
|
|
|
and print_float = pp_print_float std_formatter
|
|
|
|
and print_char = pp_print_char std_formatter
|
|
|
|
and print_bool = pp_print_bool std_formatter
|
|
|
|
and print_break = pp_print_break std_formatter
|
|
|
|
and print_cut = pp_print_cut std_formatter
|
|
|
|
and print_space = pp_print_space std_formatter
|
|
|
|
and force_newline = pp_force_newline std_formatter
|
|
|
|
and print_flush = pp_print_flush std_formatter
|
|
|
|
and print_newline = pp_print_newline std_formatter
|
|
|
|
and print_if_newline = pp_print_if_newline std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and open_tbox = pp_open_tbox std_formatter
|
|
|
|
and close_tbox = pp_close_tbox std_formatter
|
|
|
|
and print_tbreak = pp_print_tbreak std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_tab = pp_set_tab std_formatter
|
|
|
|
and print_tab = pp_print_tab std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_margin = pp_set_margin std_formatter
|
|
|
|
and get_margin = pp_get_margin std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_max_indent = pp_set_max_indent std_formatter
|
|
|
|
and get_max_indent = pp_get_max_indent std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_max_boxes = pp_set_max_boxes std_formatter
|
|
|
|
and get_max_boxes = pp_get_max_boxes std_formatter
|
1997-09-16 06:46:36 -07:00
|
|
|
and over_max_boxes = pp_over_max_boxes std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_ellipsis_text = pp_set_ellipsis_text std_formatter
|
|
|
|
and get_ellipsis_text = pp_get_ellipsis_text std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_formatter_out_channel =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_formatter_out_channel std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
2012-04-27 02:56:05 -07:00
|
|
|
and set_formatter_out_functions =
|
|
|
|
pp_set_formatter_out_functions std_formatter
|
|
|
|
and get_formatter_out_functions =
|
|
|
|
pp_get_formatter_out_functions std_formatter
|
|
|
|
|
1996-07-08 11:53:26 -07:00
|
|
|
and set_formatter_output_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_formatter_output_functions std_formatter
|
1996-07-08 11:53:26 -07:00
|
|
|
and get_formatter_output_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_get_formatter_output_functions std_formatter
|
1998-12-02 02:15:37 -08:00
|
|
|
|
1998-12-08 00:29:54 -08:00
|
|
|
and set_all_formatter_output_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_all_formatter_output_functions std_formatter
|
1998-12-08 00:29:54 -08:00
|
|
|
and get_all_formatter_output_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_get_all_formatter_output_functions std_formatter
|
2009-11-30 15:21:49 -08:00
|
|
|
|
2002-03-19 23:33:20 -08:00
|
|
|
and set_formatter_tag_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_formatter_tag_functions std_formatter
|
2002-03-19 23:33:20 -08:00
|
|
|
and get_formatter_tag_functions =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_get_formatter_tag_functions std_formatter
|
2002-03-11 14:18:20 -08:00
|
|
|
and set_print_tags =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_print_tags std_formatter
|
2002-03-22 12:43:07 -08:00
|
|
|
and get_print_tags =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_get_print_tags std_formatter
|
2002-03-19 23:33:20 -08:00
|
|
|
and set_mark_tags =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_mark_tags std_formatter
|
2002-03-22 12:43:07 -08:00
|
|
|
and get_mark_tags =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_get_mark_tags std_formatter
|
2002-05-08 06:50:29 -07:00
|
|
|
and set_tags =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_set_tags std_formatter
|
2002-03-11 14:18:20 -08:00
|
|
|
;;
|
1995-08-29 01:31:50 -07:00
|
|
|
|
2001-10-31 03:34:21 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Printf implementation.
|
|
|
|
|
|
|
|
**************************************************************)
|
2001-10-31 03:34:21 -08:00
|
|
|
|
2006-11-17 00:34:05 -08:00
|
|
|
module Sformat = Printf.CamlinternalPr.Sformat;;
|
|
|
|
module Tformat = Printf.CamlinternalPr.Tformat;;
|
2006-04-05 04:49:07 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
(* Error messages when processing formats. *)
|
|
|
|
|
|
|
|
(* Trailer: giving up at character number ... *)
|
|
|
|
let giving_up mess fmt i =
|
2011-06-20 14:46:20 -07:00
|
|
|
Printf.sprintf
|
|
|
|
"Format.fprintf: %s ``%s'', giving up at character number %d%s"
|
|
|
|
mess (Sformat.to_string fmt) i
|
|
|
|
(if i < Sformat.length fmt
|
|
|
|
then Printf.sprintf " (%c)." (Sformat.get fmt i)
|
|
|
|
else Printf.sprintf "%c" '.')
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
2002-03-05 12:56:46 -08:00
|
|
|
|
2004-12-06 22:14:49 -08:00
|
|
|
(* When an invalid format deserves a special error explanation. *)
|
2002-03-05 12:56:46 -08:00
|
|
|
let format_invalid_arg mess fmt i = invalid_arg (giving_up mess fmt i);;
|
|
|
|
|
|
|
|
(* Standard invalid format. *)
|
|
|
|
let invalid_format fmt i = format_invalid_arg "bad format" fmt i;;
|
|
|
|
|
|
|
|
(* Cannot find a valid integer into that format. *)
|
|
|
|
let invalid_integer fmt i =
|
|
|
|
invalid_arg (giving_up "bad integer specification" fmt i);;
|
|
|
|
|
2011-06-20 14:46:20 -07:00
|
|
|
(* Finding an integer size out of a sub-string of the format. *)
|
2002-03-05 12:56:46 -08:00
|
|
|
let format_int_of_string fmt i s =
|
2005-09-20 10:18:03 -07:00
|
|
|
let sz =
|
|
|
|
try int_of_string s with
|
2011-06-20 14:46:20 -07:00
|
|
|
| Failure _ -> invalid_integer fmt i in
|
2008-06-16 06:04:46 -07:00
|
|
|
size_of_int sz
|
|
|
|
;;
|
1998-12-23 10:57:55 -08:00
|
|
|
|
2002-04-22 14:54:08 -07:00
|
|
|
(* Getting strings out of buffers. *)
|
|
|
|
let get_buffer_out b =
|
2008-01-11 08:13:18 -08:00
|
|
|
let s = Buffer.contents b in
|
|
|
|
Buffer.reset b;
|
2008-06-16 06:04:46 -07:00
|
|
|
s
|
|
|
|
;;
|
2002-04-22 14:54:08 -07:00
|
|
|
|
2009-05-20 04:52:42 -07:00
|
|
|
(* [ppf] is supposed to be a pretty-printer that outputs to buffer [b]:
|
|
|
|
to extract the contents of [ppf] as a string we flush [ppf] and get the
|
|
|
|
string out of [b]. *)
|
2002-04-22 14:54:08 -07:00
|
|
|
let string_out b ppf =
|
2008-01-11 08:13:18 -08:00
|
|
|
pp_flush_queue ppf false;
|
2008-06-16 06:04:46 -07:00
|
|
|
get_buffer_out b
|
|
|
|
;;
|
2002-04-22 14:54:08 -07:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(* Applies [printer] to a formatter that outputs on a fresh buffer,
|
2004-03-05 04:15:31 -08:00
|
|
|
then returns the resulting material. *)
|
2002-04-22 14:54:08 -07:00
|
|
|
let exstring printer arg =
|
2008-01-11 08:13:18 -08:00
|
|
|
let b = Buffer.create 512 in
|
|
|
|
let ppf = formatter_of_buffer b in
|
|
|
|
printer ppf arg;
|
2008-06-16 06:04:46 -07:00
|
|
|
string_out b ppf
|
|
|
|
;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(* To turn out a character accumulator into the proper string result. *)
|
|
|
|
let implode_rev s0 = function
|
|
|
|
| [] -> s0
|
2008-06-16 06:04:46 -07:00
|
|
|
| l -> String.concat "" (List.rev (s0 :: l))
|
|
|
|
;;
|
2002-05-15 13:29:26 -07:00
|
|
|
|
2006-05-04 05:52:22 -07:00
|
|
|
(* [mkprintf] is the printf-like function generator: given the
|
2006-01-04 00:50:40 -08:00
|
|
|
- [to_s] flag that tells if we are printing into a string,
|
2006-05-04 05:52:22 -07:00
|
|
|
- the [get_out] function that has to be called to get a [ppf] function to
|
2010-05-03 02:18:20 -07:00
|
|
|
output onto,
|
|
|
|
it generates a [kprintf] function that takes as arguments a [k]
|
2006-05-04 05:52:22 -07:00
|
|
|
continuation function to be called at the end of formatting,
|
|
|
|
and a printing format string to print the rest of the arguments
|
|
|
|
according to the format string.
|
2001-10-31 03:34:21 -08:00
|
|
|
Regular [fprintf]-like functions of this module are obtained via partial
|
2006-05-04 05:52:22 -07:00
|
|
|
applications of [mkprintf]. *)
|
2013-04-24 07:56:25 -07:00
|
|
|
let mkprintf to_s get_out k fmt =
|
|
|
|
|
|
|
|
(* [out] is global to this definition of [pr], and must be shared by all its
|
|
|
|
recursive calls (if any). *)
|
|
|
|
let out = get_out fmt in
|
|
|
|
let print_as = ref None in
|
|
|
|
let outc c =
|
|
|
|
match !print_as with
|
|
|
|
| None -> pp_print_char out c
|
|
|
|
| Some size ->
|
|
|
|
pp_print_as_size out size (String.make 1 c);
|
|
|
|
print_as := None
|
|
|
|
and outs s =
|
|
|
|
match !print_as with
|
|
|
|
| None -> pp_print_string out s
|
|
|
|
| Some size ->
|
|
|
|
pp_print_as_size out size s;
|
|
|
|
print_as := None
|
|
|
|
and flush out = pp_print_flush out () in
|
|
|
|
|
|
|
|
let rec pr k n fmt v =
|
2008-01-11 08:13:18 -08:00
|
|
|
|
2006-04-05 04:49:07 -07:00
|
|
|
let len = Sformat.length fmt in
|
2005-09-20 10:18:03 -07:00
|
|
|
|
2013-04-24 07:56:25 -07:00
|
|
|
let rec doprn n i =
|
|
|
|
if i >= len then Obj.magic (k out) else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| '%' ->
|
|
|
|
Tformat.scan_format fmt v n i cont_s cont_a cont_t cont_f cont_m
|
|
|
|
| '@' ->
|
|
|
|
let i = succ i in
|
2008-01-11 08:13:18 -08:00
|
|
|
if i >= len then invalid_format fmt i else
|
2013-04-24 07:56:25 -07:00
|
|
|
begin match Sformat.get fmt i with
|
|
|
|
| '[' ->
|
|
|
|
do_pp_open_box out n (succ i)
|
|
|
|
| ']' ->
|
|
|
|
pp_close_box out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| '{' ->
|
|
|
|
do_pp_open_tag out n (succ i)
|
|
|
|
| '}' ->
|
|
|
|
pp_close_tag out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| ' ' ->
|
|
|
|
pp_print_space out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| ',' ->
|
|
|
|
pp_print_cut out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| '?' ->
|
|
|
|
pp_print_flush out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| '.' ->
|
|
|
|
pp_print_newline out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| '\n' ->
|
|
|
|
pp_force_newline out ();
|
|
|
|
doprn n (succ i)
|
|
|
|
| ';' ->
|
|
|
|
do_pp_break out n (succ i)
|
|
|
|
| '<' ->
|
|
|
|
let got_size size n i =
|
|
|
|
print_as := Some size;
|
|
|
|
doprn n (skip_gt i) in
|
|
|
|
get_int n (succ i) got_size
|
2008-01-11 08:13:18 -08:00
|
|
|
| _ -> invalid_format fmt i
|
2013-04-24 07:56:25 -07:00
|
|
|
end
|
|
|
|
| c -> outc c; doprn n (succ i)
|
|
|
|
|
|
|
|
and cont_s n s i =
|
|
|
|
outs s; doprn n i
|
|
|
|
and cont_a n printer arg i =
|
|
|
|
if to_s then
|
|
|
|
outs ((Obj.magic printer : unit -> _ -> string) () arg)
|
|
|
|
else
|
|
|
|
printer out arg;
|
|
|
|
doprn n i
|
|
|
|
and cont_t n printer i =
|
|
|
|
if to_s then
|
|
|
|
outs ((Obj.magic printer : unit -> string) ())
|
|
|
|
else
|
|
|
|
printer out;
|
|
|
|
doprn n i
|
|
|
|
and cont_f n i =
|
|
|
|
flush out; doprn n i
|
|
|
|
and cont_m n xf i =
|
|
|
|
let m =
|
|
|
|
Sformat.add_int_index
|
|
|
|
(Tformat.count_printing_arguments_of_format xf) n in
|
|
|
|
pr (Obj.magic (fun _ -> doprn m i)) n xf v
|
|
|
|
|
|
|
|
and get_int n i c =
|
|
|
|
if i >= len then invalid_integer fmt i else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| ' ' -> get_int n (succ i) c
|
|
|
|
| '%' ->
|
|
|
|
let cont_s n s i = c (format_int_of_string fmt i s) n i
|
|
|
|
and cont_a _n _printer _arg i = invalid_integer fmt i
|
|
|
|
and cont_t _n _printer i = invalid_integer fmt i
|
|
|
|
and cont_f _n i = invalid_integer fmt i
|
|
|
|
and cont_m _n _sfmt i = invalid_integer fmt i in
|
|
|
|
Tformat.scan_format fmt v n i cont_s cont_a cont_t cont_f cont_m
|
|
|
|
| _ ->
|
|
|
|
let rec get j =
|
|
|
|
if j >= len then invalid_integer fmt j else
|
|
|
|
match Sformat.get fmt j with
|
|
|
|
| '0' .. '9' | '-' -> get (succ j)
|
|
|
|
| _ ->
|
|
|
|
let size =
|
|
|
|
if j = i then size_of_int 0 else
|
|
|
|
let s = Sformat.sub fmt (Sformat.index_of_int i) (j - i) in
|
|
|
|
format_int_of_string fmt j s in
|
|
|
|
c size n j in
|
|
|
|
get i
|
|
|
|
|
|
|
|
and skip_gt i =
|
|
|
|
if i >= len then invalid_format fmt i else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| ' ' -> skip_gt (succ i)
|
|
|
|
| '>' -> succ i
|
|
|
|
| _ -> invalid_format fmt i
|
|
|
|
|
|
|
|
and get_box_kind i =
|
|
|
|
if i >= len then Pp_box, i else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| 'h' ->
|
|
|
|
let i = succ i in
|
|
|
|
if i >= len then Pp_hbox, i else
|
|
|
|
begin match Sformat.get fmt i with
|
|
|
|
| 'o' ->
|
2008-01-11 08:13:18 -08:00
|
|
|
let i = succ i in
|
2013-04-24 07:56:25 -07:00
|
|
|
if i >= len then format_invalid_arg "bad box format" fmt i else
|
2008-01-11 08:13:18 -08:00
|
|
|
begin match Sformat.get fmt i with
|
2013-04-24 07:56:25 -07:00
|
|
|
| 'v' -> Pp_hovbox, succ i
|
|
|
|
| c ->
|
|
|
|
format_invalid_arg
|
|
|
|
("bad box name ho" ^ String.make 1 c) fmt i
|
2008-01-11 08:13:18 -08:00
|
|
|
end
|
2013-04-24 07:56:25 -07:00
|
|
|
| 'v' -> Pp_hvbox, succ i
|
|
|
|
| _ -> Pp_hbox, i
|
|
|
|
end
|
|
|
|
| 'b' -> Pp_box, succ i
|
|
|
|
| 'v' -> Pp_vbox, succ i
|
|
|
|
| _ -> Pp_box, i
|
|
|
|
|
|
|
|
and get_tag_name n i c =
|
|
|
|
let rec get accu n i j =
|
|
|
|
if j >= len then
|
|
|
|
c (implode_rev
|
|
|
|
(Sformat.sub fmt (Sformat.index_of_int i) (j - i))
|
|
|
|
accu)
|
|
|
|
n j else
|
|
|
|
match Sformat.get fmt j with
|
|
|
|
| '>' ->
|
|
|
|
c (implode_rev
|
|
|
|
(Sformat.sub fmt (Sformat.index_of_int i) (j - i))
|
|
|
|
accu)
|
|
|
|
n j
|
|
|
|
| '%' ->
|
|
|
|
let s0 = Sformat.sub fmt (Sformat.index_of_int i) (j - i) in
|
|
|
|
let cont_s n s i = get (s :: s0 :: accu) n i i
|
|
|
|
and cont_a n printer arg i =
|
|
|
|
let s =
|
|
|
|
if to_s
|
|
|
|
then (Obj.magic printer : unit -> _ -> string) () arg
|
|
|
|
else exstring printer arg in
|
|
|
|
get (s :: s0 :: accu) n i i
|
|
|
|
and cont_t n printer i =
|
|
|
|
let s =
|
|
|
|
if to_s
|
|
|
|
then (Obj.magic printer : unit -> string) ()
|
|
|
|
else exstring (fun ppf () -> printer ppf) () in
|
|
|
|
get (s :: s0 :: accu) n i i
|
|
|
|
and cont_f _n i =
|
|
|
|
format_invalid_arg "bad tag name specification" fmt i
|
|
|
|
and cont_m _n _sfmt i =
|
|
|
|
format_invalid_arg "bad tag name specification" fmt i in
|
|
|
|
Tformat.scan_format fmt v n j cont_s cont_a cont_t cont_f cont_m
|
|
|
|
| _ -> get accu n i (succ j) in
|
|
|
|
get [] n i i
|
|
|
|
|
|
|
|
and do_pp_break ppf n i =
|
|
|
|
if i >= len then begin pp_print_space ppf (); doprn n i end else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| '<' ->
|
|
|
|
let rec got_nspaces nspaces n i =
|
|
|
|
get_int n i (got_offset nspaces)
|
|
|
|
and got_offset nspaces offset n i =
|
|
|
|
pp_print_break ppf (int_of_size nspaces) (int_of_size offset);
|
|
|
|
doprn n (skip_gt i) in
|
|
|
|
get_int n (succ i) got_nspaces
|
|
|
|
| _c -> pp_print_space ppf (); doprn n i
|
|
|
|
|
|
|
|
and do_pp_open_box ppf n i =
|
|
|
|
if i >= len then begin pp_open_box_gen ppf 0 Pp_box; doprn n i end else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| '<' ->
|
|
|
|
let kind, i = get_box_kind (succ i) in
|
|
|
|
let got_size size n i =
|
|
|
|
pp_open_box_gen ppf (int_of_size size) kind;
|
|
|
|
doprn n (skip_gt i) in
|
|
|
|
get_int n i got_size
|
|
|
|
| _c -> pp_open_box_gen ppf 0 Pp_box; doprn n i
|
|
|
|
|
|
|
|
and do_pp_open_tag ppf n i =
|
|
|
|
if i >= len then begin pp_open_tag ppf ""; doprn n i end else
|
|
|
|
match Sformat.get fmt i with
|
|
|
|
| '<' ->
|
|
|
|
let got_name tag_name n i =
|
|
|
|
pp_open_tag ppf tag_name;
|
|
|
|
doprn n (skip_gt i) in
|
|
|
|
get_tag_name n (succ i) got_name
|
|
|
|
| _c -> pp_open_tag ppf ""; doprn n i in
|
|
|
|
|
|
|
|
doprn n 0 in
|
|
|
|
|
|
|
|
let kpr = pr k (Sformat.index_of_int 0) in
|
|
|
|
|
|
|
|
Tformat.kapr kpr fmt
|
2008-06-16 06:04:46 -07:00
|
|
|
;;
|
1997-09-05 11:26:53 -07:00
|
|
|
|
2002-05-15 13:29:26 -07:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Defining [fprintf] and various flavors of [fprintf].
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
let kfprintf k ppf = mkprintf false (fun _ -> ppf) k;;
|
2009-09-09 08:15:03 -07:00
|
|
|
let ikfprintf k ppf = Tformat.kapr (fun _ _ -> Obj.magic (k ppf));;
|
2002-04-22 14:54:08 -07:00
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
let fprintf ppf = kfprintf ignore ppf;;
|
2009-09-10 00:41:58 -07:00
|
|
|
let ifprintf ppf = ikfprintf ignore ppf;;
|
2005-09-20 10:18:03 -07:00
|
|
|
let printf fmt = fprintf std_formatter fmt;;
|
|
|
|
let eprintf fmt = fprintf err_formatter fmt;;
|
1999-02-23 10:01:17 -08:00
|
|
|
|
2010-05-03 02:18:20 -07:00
|
|
|
let ksprintf k =
|
|
|
|
let b = Buffer.create 512 in
|
|
|
|
let k ppf = k (string_out b ppf) in
|
2013-04-25 02:14:09 -07:00
|
|
|
let ppf = formatter_of_buffer b in
|
|
|
|
let get_out _ = ppf in
|
|
|
|
mkprintf true get_out k
|
2010-05-03 02:18:20 -07:00
|
|
|
;;
|
|
|
|
|
|
|
|
let sprintf fmt = ksprintf (fun s -> s) fmt;;
|
|
|
|
|
2013-04-25 02:14:09 -07:00
|
|
|
let asprintf fmt =
|
|
|
|
let b = Buffer.create 512 in
|
|
|
|
let k ppf = string_out b ppf in
|
|
|
|
let ppf = formatter_of_buffer b in
|
|
|
|
let get_out _ = ppf in
|
|
|
|
mkprintf false get_out k fmt;;
|
|
|
|
|
2010-05-03 02:18:20 -07:00
|
|
|
(**************************************************************
|
|
|
|
|
|
|
|
Deprecated stuff.
|
|
|
|
|
|
|
|
**************************************************************)
|
|
|
|
|
2005-09-20 10:18:03 -07:00
|
|
|
let kbprintf k b =
|
2008-06-16 06:04:46 -07:00
|
|
|
mkprintf false (fun _ -> formatter_of_buffer b) k
|
|
|
|
;;
|
2003-10-27 00:59:08 -08:00
|
|
|
|
2010-05-03 02:18:20 -07:00
|
|
|
(* Deprecated error prone function bprintf. *)
|
2009-05-20 04:52:42 -07:00
|
|
|
let bprintf b =
|
|
|
|
let k ppf = pp_flush_queue ppf false in
|
|
|
|
kbprintf k b
|
|
|
|
;;
|
2005-09-20 10:18:03 -07:00
|
|
|
|
2010-05-03 02:18:20 -07:00
|
|
|
(* Deprecated alias for ksprintf. *)
|
2009-09-10 00:41:58 -07:00
|
|
|
let kprintf = ksprintf;;
|
|
|
|
|
2012-04-27 02:56:05 -07:00
|
|
|
(* Output everything left in the pretty printer queue at end of execution. *)
|
2008-06-16 06:04:46 -07:00
|
|
|
at_exit print_flush
|
|
|
|
;;
|