diff options
Diffstat (limited to 'stdlib/format.ml')
| -rw-r--r-- | stdlib/format.ml | 471 |
1 files changed, 471 insertions, 0 deletions
diff --git a/stdlib/format.ml b/stdlib/format.ml new file mode 100644 index 000000000..ca631fdd2 --- /dev/null +++ b/stdlib/format.ml @@ -0,0 +1,471 @@ +(* 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 val 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 val for default tokens size *) +let pp_infinity = 9999 + +(* Global variables: default initialization is + set_margin 78 + set_min_space_left 0 *) +(* val 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 val 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 val 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 val of) width blanks are printed. + To do (?) : add a maximum width and offset val *) +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() |