From acdf61dad7415921dae81ae59176519a77e972f6 Mon Sep 17 00:00:00 2001 From: Pierre Weis Date: Fri, 5 Mar 2004 12:15:31 +0000 Subject: [PATCH] Hardening the behaviour of pp_print_flush. git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@6134 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02 --- stdlib/format.ml | 181 +++++++++++++++++++++++++---------------------- 1 file changed, 95 insertions(+), 86 deletions(-) diff --git a/stdlib/format.ml b/stdlib/format.ml index cc22c2c51..9d2ce5192 100644 --- a/stdlib/format.ml +++ b/stdlib/format.ml @@ -57,12 +57,12 @@ and tblock = Pp_tbox of int list ref (* Tabulation box *) 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 *) + 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 *) + is the value of pp_left_total when the element has been enqueued. *) type pp_scan_elem = Scan_elem of int * pp_queue_elem;; (* Formatting stack: @@ -71,7 +71,7 @@ type pp_scan_elem = Scan_elem of int * pp_queue_elem;; the currently active blocks. *) type pp_format_elem = Format_elem of block_type * int;; -(* General purpose queues, used in the formatter *) +(* General purpose queues, used in the formatter. *) type 'a queue_elem = | Nil | Cons of 'a queue_cell and 'a queue_cell = {mutable head : 'a; mutable tail : 'a queue_elem};; @@ -98,37 +98,37 @@ type formatter = { mutable pp_mark_stack : tag list; (* Global variables: default initialization is set_margin 78 - set_min_space_left 0 *) - (* Value of right margin *) + set_min_space_left 0. *) + (* Value of right margin. *) mutable pp_margin : int; - (* Minimal space left before margin, when opening a block *) + (* 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 *) + no blocks can be opened further. *) mutable pp_max_indent : int; - (* Space remaining on the current line *) + (* Space remaining on the current line. *) mutable pp_space_left : int; - (* Current value of indentation *) + (* Current value of indentation. *) mutable pp_current_indent : int; - (* True when the line has been broken by the pretty-printer *) + (* True when the line has been broken by the pretty-printer. *) mutable pp_is_new_line : bool; - (* Total width of tokens already printed *) + (* Total width of tokens already printed. *) mutable pp_left_total : int; - (* Total width of tokens ever put in queue *) + (* Total width of tokens ever put in queue. *) mutable pp_right_total : int; - (* Current number of opened blocks *) + (* Current number of opened blocks. *) mutable pp_curr_depth : int; - (* Maximum number of blocks which can be simultaneously opened *) + (* Maximum number of blocks which can be simultaneously opened. *) mutable pp_max_boxes : int; - (* Ellipsis string *) + (* Ellipsis string. *) mutable pp_ellipsis : string; - (* Output function *) + (* Output function. *) mutable pp_output_function : string -> int -> int -> unit; - (* Flushing function *) + (* Flushing function. *) mutable pp_flush_function : unit -> unit; - (* Output of new lines *) + (* Output of new lines. *) mutable pp_output_newline : unit -> unit; - (* Output of indentation spaces *) + (* Output of indentation spaces. *) mutable pp_output_spaces : int -> unit; (* Are tags printed ? *) mutable pp_print_tags : bool; @@ -139,7 +139,7 @@ type formatter = { 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 *) + (* The pretty-printer queue. *) mutable pp_queue : pp_queue_elem queue };; @@ -159,7 +159,7 @@ let add_queue x q = let c = Cons {head = x; tail = Nil} in match q with | {insert = Cons cell} -> q.insert <- c; cell.tail <- c - (* Invariant: when insert is Nil body should be Nil *) + (* Invariant: when insert is Nil body should be Nil. *) | _ -> q.insert <- c; q.body <- c;; exception Empty_queue;; @@ -171,11 +171,11 @@ let peek_queue = function let take_queue = function | {body = Cons {head = x; tail = tl}} as q -> q.body <- tl; - if tl = Nil then q.insert <- Nil; (* Maintain the invariant *) + if tl = Nil then q.insert <- Nil; (* Maintain the invariant. *) x | _ -> raise Empty_queue;; -(* Enter a token in the pretty-printer queue *) +(* Enter a token in the pretty-printer queue. *) let pp_enqueue state ({length = len} as token) = state.pp_right_total <- state.pp_right_total + len; add_queue token state.pp_queue;; @@ -184,32 +184,32 @@ let pp_clear_queue state = state.pp_left_total <- 1; state.pp_right_total <- 1; clear_queue state.pp_queue;; -(* Large value for default tokens size *) +(* Large value for default tokens size. *) (* Could be 1073741823 that is 2^30 - 1, that is the minimal upper bound of integers; now that max_int is defined, could also be max_int - 1. *) let pp_infinity = 1000000000;; -(* Output functions for the formatter *) +(* Output functions for the formatter. *) let pp_output_string state s = state.pp_output_function s 0 (String.length s) and pp_output_newline state = state.pp_output_newline ();; let pp_display_blanks state n = state.pp_output_spaces n;; -(* To format a break, indenting a new line *) +(* To format a break, indenting a new line. *) let break_new_line state offset width = 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 *) + (* 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; pp_display_blanks state state.pp_current_indent;; -(* To force a line break inside a block: no offset is added *) +(* To force a line break inside a block: no offset is added. *) let break_line state width = break_new_line state 0 width;; -(* To format a break that fits on the current line *) +(* To format a break that fits on the current line. *) let break_same_line state width = state.pp_space_left <- state.pp_space_left - width; pp_display_blanks state width;; @@ -225,9 +225,9 @@ let pp_force_break_line state = | Pp_fits -> () | Pp_hbox -> () | _ -> break_line state width) | _ -> pp_output_newline state;; -(* To skip a token, if the previous line has been broken *) +(* To skip a token, if the previous line has been broken. *) let pp_skip_token state = - (* When calling pp_skip_token the queue cannot be empty *) + (* When calling pp_skip_token the queue cannot be empty. *) match take_queue state.pp_queue with {elem_size = size; length = len} -> state.pp_left_total <- state.pp_left_total - len; @@ -239,7 +239,7 @@ let pp_skip_token state = **************************************************************) -(* To format a token *) +(* To format a token. *) let format_pp_token state size = function | Pp_text s -> @@ -250,7 +250,7 @@ let format_pp_token state size = function | Pp_begin (off, ty) -> 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 *) + (* 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 = @@ -264,7 +264,7 @@ let format_pp_token state size = function | Pp_end -> begin match state.pp_format_stack with | x :: (y :: l as ls) -> state.pp_format_stack <- ls - | _ -> () (* No more block to close *) + | _ -> () (* No more block to close. *) end | Pp_tbegin (Pp_tbox _ as tbox) -> @@ -273,7 +273,7 @@ let format_pp_token state size = function | Pp_tend -> begin match state.pp_tbox_stack with | x :: ls -> state.pp_tbox_stack <- ls - | _ -> () (* No more tabulation block to close *) + | _ -> () (* No more tabulation block to close. *) end | Pp_stab -> @@ -283,7 +283,7 @@ let format_pp_token state size = 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 - | _ -> () (* No opened tabulation block *) + | _ -> () (* No opened tabulation block. *) end | Pp_tbreak (n, off) -> @@ -301,7 +301,7 @@ let format_pp_token state size = function 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 - | _ -> () (* No opened tabulation block *) + | _ -> () (* No opened tabulation block. *) end | Pp_newline -> @@ -336,7 +336,7 @@ let format_pp_token state size = function | Pp_vbox -> break_new_line state off width | Pp_hbox -> break_same_line state n end - | _ -> () (* No opened block *) + | _ -> () (* No opened block. *) end | Pp_open_tag tag_name -> @@ -350,13 +350,13 @@ let format_pp_token state size = function let marker = state.pp_mark_close_tag tag_name in pp_output_string state marker; state.pp_mark_stack <- tags - | _ -> () (* No more tag to close *) + | _ -> () (* No more tag to close. *) end;; -(* Print if token size is known or printing is delayed - Size is known when not negative +(* 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 exists on the current line *) + more room to format than exists on the current line. *) let rec advance_left state = try match peek_queue state.pp_queue with @@ -374,33 +374,33 @@ let rec advance_left state = let enqueue_advance state tok = pp_enqueue state tok; advance_left state;; -(* To enqueue a string : try to advance *) +(* To enqueue a string : try to advance. *) let enqueue_string_as state n s = enqueue_advance state {elem_size = n; token = Pp_text s; length = n};; let enqueue_string state s = enqueue_string_as state (String.length s) s;; (* Routines for scan stack - determine sizes of blocks *) + determine sizes of blocks. *) -(* The scan_stack is never empty *) +(* The scan_stack is never empty. *) let scan_stack_bottom = [Scan_elem (-1, {elem_size = (-1); token = Pp_text ""; length = 0})];; (* 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 *) + if ty = true then size of break is set else size of block is set; + in each case pp_scan_stack is popped. *) let clear_scan_stack state = state.pp_scan_stack <- scan_stack_bottom;; (* 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 *) + since scan_push is used on breaks and opening of boxes. *) let set_size state ty = match state.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 *) + (* 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 (_, _) -> @@ -415,11 +415,11 @@ let set_size state ty = queue_elem.elem_size <- state.pp_right_total + size; state.pp_scan_stack <- t end - | _ -> () (* scan_push is only used for breaks and boxes *) + | _ -> () (* scan_push is only used for breaks and boxes. *) end - | _ -> () (* scan_stack is never empty *);; + | _ -> () (* scan_stack is never empty. *);; -(* Push a token on scan stack. If b is true set_size is called *) +(* Push a token on scan stack. If b is true set_size is called. *) let scan_push state b tok = pp_enqueue state tok; if b then set_size state true; @@ -428,7 +428,7 @@ let scan_push state b tok = (* To open a new block : the user may set the depth bound pp_max_boxes - any text nested deeper is printed as the ellipsis string *) + any text nested deeper is printed as the ellipsis string. *) let pp_open_box_gen state indent br_ty = state.pp_curr_depth <- state.pp_curr_depth + 1; if state.pp_curr_depth < state.pp_max_boxes then @@ -438,14 +438,14 @@ let pp_open_box_gen state indent br_ty = if state.pp_curr_depth = state.pp_max_boxes then enqueue_string state state.pp_ellipsis;; -(* The box which is always opened *) +(* The box which is always opened. *) let pp_open_sys_box state = state.pp_curr_depth <- state.pp_curr_depth + 1; scan_push state false {elem_size = (- state.pp_right_total); token = Pp_begin (0, Pp_hovbox); length = 0};; -(* Close a block, setting sizes of its subblocks *) +(* Close a block, setting sizes of its subblocks. *) let pp_close_box state () = if state.pp_curr_depth > 1 then begin @@ -475,7 +475,7 @@ let pp_close_tag state () = | tag_name :: tags -> state.pp_print_close_tag tag_name; state.pp_tag_stack <- tags - | _ -> () (* No more tag to close *) + | _ -> () (* No more tag to close. *) end;; let pp_set_print_tags state b = state.pp_print_tags <- b;; @@ -506,13 +506,13 @@ let pp_set_formatter_tag_functions state { let pp_rinit state = pp_clear_queue state; clear_scan_stack state; - state.pp_current_indent <- 0; - state.pp_curr_depth <- 0; - state.pp_space_left <- state.pp_margin; 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;; (* Flushing pretty-printer queue. *) @@ -522,8 +522,17 @@ let pp_flush_queue state b = done; state.pp_right_total <- pp_infinity; advance_left state; - if b then pp_output_newline state; - if b then pp_rinit state;; + if b then begin + pp_output_newline state; + pp_rinit state + end else begin + clear_scan_stack state; + state.pp_format_stack <- []; + state.pp_current_indent <- 0; + state.pp_curr_depth <- 0; + state.pp_space_left <- state.pp_margin; + pp_open_sys_box state; + end;; (************************************************************** @@ -531,27 +540,27 @@ let pp_flush_queue state b = **************************************************************) -(* To format a string *) +(* To format a string. *) let pp_print_as state n s = if state.pp_curr_depth < state.pp_max_boxes then enqueue_string_as state n s;; let pp_print_string state s = pp_print_as state (String.length s) s;; -(* To format an integer *) +(* To format an integer. *) let pp_print_int state i = pp_print_string state (string_of_int i);; -(* To format a float *) +(* To format a float. *) let pp_print_float state f = pp_print_string state (string_of_float f);; -(* To format a boolean *) +(* To format a boolean. *) let pp_print_bool state b = pp_print_string state (string_of_bool b);; -(* To format a char *) +(* To format a char. *) let pp_print_char state c = let s = String.create 1 in s.[0] <- c; pp_print_as state 1 s;; -(* Opening boxes *) +(* Opening boxes. *) 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 @@ -560,18 +569,18 @@ 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;; (* Print a new line after printing all queued text - (same for print_flush but without a newline). *) + (same for print_flush but without a newline). *) let pp_print_newline state () = pp_flush_queue state true; state.pp_flush_function () and pp_print_flush state () = pp_flush_queue state false; state.pp_flush_function ();; -(* To get a newline when one does not want to close the current block *) +(* To get a newline when one does not want to close the current block. *) let pp_force_newline state () = if state.pp_curr_depth < state.pp_max_boxes then enqueue_advance state {elem_size = 0; token = Pp_newline; length = 0};; -(* To format something if the line has just been broken *) +(* To format something if the line has just been broken. *) let pp_print_if_newline state () = if state.pp_curr_depth < state.pp_max_boxes then enqueue_advance state {elem_size = 0; token = Pp_if_newline; length = 0};; @@ -579,7 +588,7 @@ let pp_print_if_newline state () = (* 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 *) + To do (?) : add a maximum width and offset value. *) let pp_print_break state width offset = if state.pp_curr_depth < state.pp_max_boxes then scan_push state true @@ -589,7 +598,7 @@ let pp_print_break state width offset = let pp_print_space state () = pp_print_break state 1 0 and pp_print_cut state () = pp_print_break state 0 0;; -(* Tabulation boxes *) +(* Tabulation boxes. *) let pp_open_tbox state () = state.pp_curr_depth <- state.pp_curr_depth + 1; if state.pp_curr_depth < state.pp_max_boxes then @@ -597,14 +606,14 @@ let pp_open_tbox state () = {elem_size = 0; token = Pp_tbegin (Pp_tbox (ref [])); length = 0};; -(* Close a tabulation block *) +(* Close a tabulation block. *) let pp_close_tbox state () = if state.pp_curr_depth > 1 then begin if state.pp_curr_depth < state.pp_max_boxes then enqueue_advance state {elem_size = 0; token = Pp_tend; length = 0}; state.pp_curr_depth <- state.pp_curr_depth - 1 end;; -(* Print a tabulation break *) +(* Print a tabulation break. *) let pp_print_tbreak state width offset = if state.pp_curr_depth < state.pp_max_boxes then scan_push state true @@ -623,19 +632,19 @@ let pp_set_tab state () = **************************************************************) -(* Fit max_boxes *) +(* Fit max_boxes. *) let pp_set_max_boxes state n = if n > 1 then state.pp_max_boxes <- n;; -(* To know the current maximum number of boxes allowed *) +(* To know the current maximum number of boxes allowed. *) let pp_get_max_boxes state () = state.pp_max_boxes;; let pp_over_max_boxes state () = state.pp_curr_depth = state.pp_max_boxes;; -(* Ellipsis *) +(* Ellipsis. *) let pp_set_ellipsis_text state s = state.pp_ellipsis <- s and pp_get_ellipsis_text state () = state.pp_ellipsis;; -(* To set the margin of pretty-printer *) +(* To set the margin of pretty-printer. *) let pp_set_min_space_left state n = if n >= 1 && n < pp_infinity then begin state.pp_min_space_left <- n; @@ -644,7 +653,7 @@ let pp_set_min_space_left state n = (* Initially, we have : pp_max_indent = pp_margin - pp_min_space_left, and - pp_space_left = pp_margin *) + pp_space_left = pp_margin. *) let pp_set_max_indent state n = pp_set_min_space_left state (state.pp_margin - n);; let pp_get_max_indent state () = state.pp_max_indent;; @@ -653,15 +662,15 @@ let pp_set_margin state n = if n >= 1 && n < pp_infinity then begin state.pp_margin <- n; let new_max_indent = - (* Try to maintain max_indent to its actual value *) + (* 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 *) + new margin, if it is greater than 1. *) max (max (state.pp_margin - state.pp_min_space_left) (state.pp_margin / 2)) 1 in - (* Rebuild invariants *) + (* Rebuild invariants. *) pp_set_max_indent state new_max_indent end;; let pp_get_margin state () = state.pp_margin;; @@ -697,7 +706,7 @@ let default_pp_print_open_tag s = ();; let default_pp_print_close_tag = default_pp_print_open_tag;; let pp_make_formatter f g h i = - (* The initial state of the formatter contains a dummy box *) + (* The initial state of the formatter contains a dummy box. *) let pp_q = make_queue () in let sys_tok = {elem_size = (- 1); token = Pp_begin (0, Pp_hovbox); length = 0} in @@ -733,7 +742,7 @@ let pp_make_formatter f g h i = pp_queue = pp_q };; -(* Default function to output spaces *) +(* Default function to output spaces. *) let blank_line = String.make 80 ' ';; let rec display_blanks state n = if n > 0 then @@ -743,7 +752,7 @@ let rec display_blanks state n = display_blanks state (n - 80) end;; -(* Default function to output new lines *) +(* Default function to output new lines. *) let display_newline state () = state.pp_output_function "\n" 0 1;; let make_formatter f g = @@ -895,7 +904,7 @@ let string_out b ppf = get_buffer_out b;; (* Applies [printer] to a formatter that outputs on a fresh buffer, - then returns the resulting material *) + then returns the resulting material. *) let exstring printer arg = let b = Buffer.create 512 in let ppf = formatter_of_buffer b in