ocaml/stdlib/format.ml

472 lines
16 KiB
OCaml
Raw Normal View History

(* Tokens are one of the following : *)
type pp_token =
Pp_text of string (* normal text *)
| Pp_break of int * int (* complete break *)
| Pp_tbreak of int * int (* go to next tab *)
| Pp_stab (* set a tabulation *)
| Pp_begin of int * block_type (* beginning of a block *)
| Pp_end (* end of a block *)
| Pp_tbegin of tblock (* Beginning of a tabulation block *)
| 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 *)
and block_type =
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_fits (* Internal usage: when a block fits on a single line *)
and tblock = Pp_tbox of int list ref (* Tabulation box *)
(* The Queue: contains all formatting elements.
elements are tuples (size,token,length), where
size is set when the size of the block is known
len is the declared length of the token *)
type pp_queue_elem =
{mutable elem_size : int; token : pp_token; length : int}
(* Scan stack
each element is (left_total, queue element) where left_total
is the value of pp_left_total when the element has been enqueued *)
type pp_scan_elem = Scan_elem of int * pp_queue_elem
let pp_scan_stack = ref ([] : pp_scan_elem list)
(* Formatting Stack:
used to break the lines while printing tokens.
The formatting stack contains the description of
the currently active blocks. *)
type pp_format_elem = Format_elem of block_type * int
let pp_format_stack = ref ([]:pp_format_elem list)
let pp_tbox_stack = ref ([]:tblock list)
(* Large value for default tokens size *)
let pp_infinity = 9999
(* Global variables: default initialization is
set_margin 78
set_min_space_left 0 *)
(* value of right margin *)
let pp_margin = ref 78
(* Minimal space left before margin, when opening a block *)
let pp_min_space_left = ref 10
(* maximum value of indentation:
no blocks can be opened further *)
let pp_max_indent = ref (!pp_margin - !pp_min_space_left)
let pp_space_left = ref !pp_margin(* space remaining on the current line *)
and pp_current_indent = ref 0 (* current value of indentation *)
and pp_left_total = ref 1 (* total width of tokens already printed *)
and pp_right_total = ref 1 (* total width of tokens ever put in queue *)
and pp_curr_depth = ref 0 (* current number of opened blocks *)
and pp_max_boxes = ref 35 (* maximum number of blocks which can be
opened at the same time *)
and pp_ellipsis = ref "." (* ellipsis string *)
and pp_out_channel = ref stdout (* out_channel of the pretty_printer *)
(* Output functions for the formatter *)
let pp_output s = output !pp_out_channel s
and pp_output_string s = output_string !pp_out_channel s
and pp_output_newline () = output_char !pp_out_channel '\n'
(* The pretty-printer queue *)
let pp_queue = (Queue.new () : pp_queue_elem Queue.t)
let pp_clear_queue () =
pp_left_total := 1; pp_right_total := 1;
Queue.clear pp_queue
(* Enter a token in the pretty-printer queue *)
let pp_enqueue ({length=len} as token) =
pp_right_total := !pp_right_total + len;
Queue.add token pp_queue
(* To output spaces *)
let blank_line = String.make 80 ' '
let display_blanks n =
if n > 0 then
if n <= 80 then pp_output blank_line 0 n
else pp_output_string (String.make n ' ')
(* To format a break, indenting a new line *)
let break_new_line offset width =
pp_output_newline ();
let indent = !pp_margin - width + offset in
(* Don't indent more than pp_max_indent *)
let real_indent = min !pp_max_indent indent in
pp_current_indent := real_indent;
pp_space_left := !pp_margin - !pp_current_indent;
display_blanks !pp_current_indent
(* To force a line break inside a block: no offset is added *)
let break_line width = break_new_line 0 width
(* To format a break that fits on the current line *)
let break_same_line width =
pp_space_left := !pp_space_left - width;
display_blanks width
(* 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. *)
let pp_force_newline () =
match !pp_format_stack with
Format_elem (bl_ty, width) :: _ ->
if width > !pp_space_left then
(match bl_ty with
Pp_fits -> () | Pp_hbox -> () | _ -> break_line width)
| _ -> pp_output_newline()
(* To skip a token, if the previous line has been broken *)
let pp_skip_token () =
(* When calling pp_skip_token the queue cannot be empty *)
match Queue.take pp_queue with
{elem_size = size; length = len} ->
pp_left_total := !pp_left_total - len;
pp_space_left := !pp_space_left + size
(* To format a token *)
let format_pp_token size = function
Pp_text s -> pp_space_left := !pp_space_left - size; pp_output_string s
| Pp_begin (off,ty) ->
let insertion_point = !pp_margin - !pp_space_left in
if insertion_point > !pp_max_indent then
(* can't open a block right there ! *)
pp_force_newline () else
(* If block is rejected on the left current indentation will change *)
if size > !pp_space_left & !pp_current_indent < insertion_point then
pp_force_newline ();
let offset = !pp_space_left - off in
let bl_type =
begin match ty with
Pp_vbox -> Pp_vbox
| _ -> if size > !pp_space_left then ty else Pp_fits
end in
pp_format_stack := Format_elem (bl_type, offset) :: !pp_format_stack
| Pp_end ->
begin match !pp_format_stack with
x::(y::l as ls) -> pp_format_stack := ls
| _ -> () (* No more block to close *)
end
| Pp_tbegin (Pp_tbox _ as tbox) -> pp_tbox_stack := tbox :: !pp_tbox_stack
| Pp_tend ->
begin match !pp_tbox_stack with
x::ls -> pp_tbox_stack := ls
| _ -> () (* No more tabulation block to close *)
end
| Pp_stab ->
begin match !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 (!pp_margin - !pp_space_left) !tabs
| _ -> () (* No opened tabulation block *)
end
| Pp_tbreak (n,off) ->
let insertion_point = !pp_margin - !pp_space_left in
begin match !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
x :: l ->
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 (offset + n) else
break_new_line (tab + off) !pp_margin
| _ -> () (* No opened tabulation block *)
end
| Pp_newline ->
begin match !pp_format_stack with
Format_elem (_,width) :: _ -> break_line width
| _ -> pp_output_newline()
end
| Pp_if_newline ->
if !pp_current_indent != !pp_margin - !pp_space_left
then pp_skip_token ()
| Pp_break (n,off) ->
begin match !pp_format_stack with
Format_elem (ty,width) :: _ ->
begin match ty with
Pp_hovbox ->
if size > !pp_space_left then break_new_line off width else
(* break the line here leads to new indentation ? *)
if (!pp_current_indent > !pp_margin - width + off)
then break_new_line off width else break_same_line n
| Pp_hvbox -> break_new_line off width
| Pp_fits -> break_same_line n
| Pp_vbox -> break_new_line off width
| Pp_hbox -> break_same_line n
end
| _ -> () (* No opened block *)
end
(* Print if token size is known or printing is delayed
Size is known when not negative
Printing is delayed when the text waiting in the queue requires
more room to format than List.exists on the current line *)
let rec advance_left () =
try
match Queue.peek pp_queue with
{elem_size = size; token = tok; length = len} ->
if not (size < 0 &
(!pp_right_total - !pp_left_total <= !pp_space_left)) then
begin
Queue.take pp_queue;
format_pp_token (if size < 0 then pp_infinity else size) tok;
pp_left_total := len + !pp_left_total;
advance_left ()
end
with Queue.Empty -> ()
let enqueue_advance tok = pp_enqueue tok; advance_left ()
(* To enqueue a string : try to advance *)
let enqueue_string_as n s =
enqueue_advance {elem_size = n; token = Pp_text s; length = n}
let enqueue_string s = enqueue_string_as (String.length s) s
(* Routines for scan stack
determine sizes of blocks *)
(* scan_stack is never empty *)
let empty_scan_stack =
[Scan_elem (-1, {elem_size = (-1); token = Pp_text ""; length = 0})]
let clear_scan_stack () = pp_scan_stack := empty_scan_stack
(* Set size of blocks on scan stack:
if ty = true then size of break is set else size of block is set
in each case pp_scan_stack is popped *)
(* Pattern matching on scan stack is exhaustive,
since scan_stack is never empty.
Pattern matching on token in scan stack is also exhaustive,
since scan_push is used on breaks and opening of boxes *)
let set_size ty =
match !pp_scan_stack with
Scan_elem (left_tot,
({elem_size = size; token = tok} as queue_elem)) :: t ->
(* test if scan stack contains any data that is not obsolete *)
if left_tot < !pp_left_total then clear_scan_stack () else
begin match tok with
Pp_break (_, _) | Pp_tbreak (_, _) ->
if ty then
begin
queue_elem.elem_size <- !pp_right_total + size;
pp_scan_stack := t
end
| Pp_begin (_, _) ->
if not ty then
begin
queue_elem.elem_size <- !pp_right_total + size;
pp_scan_stack := t
end
| _ -> () (* scan_push is only used for breaks and boxes *)
end
| _ -> () (* scan_stack is never empty *)
(* Push a token on scan stack. If b is true set_size is called *)
let scan_push b tok =
pp_enqueue tok;
if b then set_size true;
pp_scan_stack := Scan_elem (!pp_right_total,tok) :: !pp_scan_stack
(*
To open a new block :
the user may set the depth bound pp_max_boxes
any text nested deeper is printed as the character the ellipsis
*)
let pp_open_box (indent,br_ty) =
incr pp_curr_depth;
if !pp_curr_depth < !pp_max_boxes then
(scan_push false
{elem_size = (- !pp_right_total);
token = Pp_begin (indent, br_ty); length = 0}) else
if !pp_curr_depth = !pp_max_boxes then enqueue_string !pp_ellipsis
(* The box which is always opened *)
let pp_open_sys_box () =
incr pp_curr_depth;
scan_push false
{elem_size = (- !pp_right_total);
token = Pp_begin (0, Pp_hovbox); length = 0}
(* close a block, setting sizes of its subblocks *)
let close_box () =
if !pp_curr_depth > 1 then
begin
if !pp_curr_depth < !pp_max_boxes then
begin
pp_enqueue {elem_size = 0; token = Pp_end; length = 0};
set_size true; set_size false
end;
decr pp_curr_depth
end
(* Initialize pretty-printer. *)
let pp_rinit () =
pp_clear_queue ();
clear_scan_stack();
pp_current_indent := 0;
pp_curr_depth := 0; pp_space_left := !pp_margin;
pp_format_stack := [];
pp_tbox_stack := [];
pp_open_sys_box ()
(* Flushing pretty-printer queue. *)
let pp_flush b =
while !pp_curr_depth > 1 do
close_box ()
done;
pp_right_total := pp_infinity; advance_left ();
if b then pp_output_newline ();
flush !pp_out_channel;
pp_rinit()
(**************************************************************
Procedures to format objects, and use boxes
**************************************************************)
(* To format a string *)
let print_as n s =
if !pp_curr_depth < !pp_max_boxes then (enqueue_string_as n s)
let print_string s = print_as (String.length s) s
(* To format an integer *)
let print_int i = print_string (string_of_int i)
(* To format a float *)
let print_float f = print_string (string_of_float f)
(* To format a boolean *)
let print_bool b = print_string (string_of_bool b)
(* To format a char *)
let print_char c = print_string (String.make 1 c)
let open_hbox () = pp_open_box (0, Pp_hbox)
and open_vbox indent = pp_open_box (indent, Pp_vbox)
and open_hvbox indent = pp_open_box (indent, Pp_hvbox)
and open_hovbox indent = pp_open_box (indent, Pp_hovbox)
(* Print a new line after printing all queued text
(same for print_flush but without a newline) *)
let print_newline () = pp_flush true
and print_flush () = pp_flush false
(* To get a newline when one does not want to close the current block *)
let force_newline () =
if !pp_curr_depth < !pp_max_boxes
then enqueue_advance {elem_size = 0; token = Pp_newline; length = 0}
(* To format something if the line has just been broken *)
let print_if_newline () =
if !pp_curr_depth < !pp_max_boxes
then enqueue_advance {elem_size = 0; token = Pp_if_newline ;length = 0}
(* Breaks: indicate where a block may be broken.
If line is broken then offset is added to the indentation of the current
block else (the value of) width blanks are printed.
To do (?) : add a maximum width and offset value *)
let print_break width offset =
if !pp_curr_depth < !pp_max_boxes then
scan_push true
{elem_size = (- !pp_right_total); token = Pp_break (width,offset);
length = width}
let print_space () = print_break 1 0
and print_cut () = print_break 0 0
let open_tbox () =
incr pp_curr_depth;
if !pp_curr_depth < !pp_max_boxes then
enqueue_advance
{elem_size = 0;
token = Pp_tbegin (Pp_tbox (ref [])); length = 0}
(* Close a tabulation block *)
let close_tbox () =
if !pp_curr_depth > 1 then begin
if !pp_curr_depth < !pp_max_boxes then
enqueue_advance {elem_size = 0; token = Pp_tend; length = 0};
decr pp_curr_depth end
(* Print a tabulation break *)
let print_tbreak width offset =
if !pp_curr_depth < !pp_max_boxes then
scan_push true
{elem_size = (- !pp_right_total); token = Pp_tbreak (width,offset);
length = width}
let print_tab () = print_tbreak 0 0
let set_tab () =
if !pp_curr_depth < !pp_max_boxes
then enqueue_advance {elem_size = 0; token = Pp_stab; length=0}
(**************************************************************
Procedures to control the pretty-printer
**************************************************************)
(* Fit max_boxes *)
let set_max_boxes n = if n > 1 then pp_max_boxes := n
(* To know the current maximum number of boxes allowed *)
let get_max_boxes () = !pp_max_boxes
(* Ellipsis *)
let set_ellipsis_text s = pp_ellipsis := s
and get_ellipsis_text () = !pp_ellipsis
(* To set the margin of pretty-formater *)
let set_margin n =
if n >= 1 then
begin
pp_margin := n;
pp_max_indent := !pp_margin - !pp_min_space_left;
pp_rinit () end
let get_margin () = !pp_margin
let set_min_space_left n =
if n >= 1 then
begin
pp_min_space_left := n;
pp_max_indent := !pp_margin - !pp_min_space_left;
pp_rinit () end
let set_max_indent n = set_min_space_left (!pp_margin - n)
let get_max_indent () = !pp_max_indent
let set_formatter_output os = pp_out_channel := os
let get_formatter_output () = !pp_out_channel
(* Initializing formatter *)
let _ = pp_rinit()