From af74d6bb205ee227a100d8218ed6e66f5e78eccc Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 24 May 2011 16:40:35 +0000 Subject: [PATCH] Fixed box pretty printing. --- matitaB/components/content_pres/boxPp.ml | 59 +++++++++++++----------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml index 5d406b9fb..ff9464996 100644 --- a/matitaB/components/content_pres/boxPp.ml +++ b/matitaB/components/content_pres/boxPp.ml @@ -28,7 +28,8 @@ (** {2 Pretty printing from BoxML to strings} *) -let utf8_string_length s = Utf8.compute_len s 0 (String.length s) +let utf8_string_length s = + Utf8.compute_len s 0 (String.length s) let string_space = " " let string_space_len = utf8_string_length string_space @@ -64,39 +65,40 @@ let merge_columns sep cols = let sep_len = utf8_string_length sep in let indent = ref 0 in let res_rows = ref [] in - let add_row ~continue row = + let max_len = ref 0 in + let add_row ~continue size row = match !res_rows with | last :: prev when continue -> res_rows := (last ^ sep ^ row) :: prev; - indent := !indent + utf8_string_length last + sep_len + indent := size | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows; in List.iter - (fun rows -> - match rows with + (fun (len,rows) -> + (match rows with | hd :: tl -> - add_row ~continue:true hd; - List.iter (add_row ~continue:false) tl - | [] -> ()) + add_row ~continue:true !max_len hd; + List.iter (add_row ~continue:false len) tl + | [] -> ()); + max_len := !max_len + len + sep_len) cols; - List.rev !res_rows + !max_len, List.rev !res_rows -let max_len = - List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0 - let render_row available_space spacing children = let spacing_bonus = if spacing then string_space_len else 0 in let rem_space = ref available_space in let renderings = ref [] in List.iter (fun f -> - let occupied_space, rendering = f !rem_space in + let (*occupied_space, rendering*) rendering = f !rem_space in + let occupied_space,_ = rendering in renderings := rendering :: !renderings; rem_space := !rem_space - (occupied_space + spacing_bonus)) children; let sep = if spacing then string_space else "" in - let rendering = merge_columns sep (List.rev !renderings) in - max_len rendering, rendering + (*let rendering = merge_columns sep (List.rev !renderings) in + max_len rendering, rendering *) + merge_columns sep (List.rev !renderings) let fixed_rendering s = let s_len = utf8_string_length s in @@ -158,7 +160,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let hd_f = aux_box hd in let tl_fs = List.map aux_box tl in (fun size -> - let hd_rendering = snd (hd_f size) in + let hd_rendering = hd_f size in let children_size = max 0 (if indent then size - string_indent_len else size) in @@ -166,11 +168,12 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = List.map (fun f -> (* let indent_header = if indent then string_indent else "" in *) - snd (indent_children (f children_size))) + indent_children (f children_size)) tl_fs in - let rows = hd_rendering @ List.concat tl_renderings in - max_len rows, rows) + List.fold_right + (fun (len,row) (acclen,accrows) -> max acclen len, row@accrows) + (hd_rendering::tl_renderings) (0,[])) | Box.HOV (attrs, []) -> assert false | Box.HOV (attrs, [child]) -> aux_box child | Box.HOV (attrs, children) -> @@ -185,19 +188,23 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let renderings = ref [] in let rem_space = ref size in let first_row = ref true in - let use_rendering (space, rendering) = + let max_len = ref 0 in + let use_rendering (* (space, rendering) *) rendering = + let space, _ = rendering in let use_indent = !renderings = [] && not !first_row in - let rendering' = - if use_indent then List.map indent_string rendering - else rendering + let bonus = if use_indent then indent_bonus else spacing_bonus in + let rendering' = (* space+bonus, *) + if use_indent then + space+indent_bonus, List.map indent_string (snd rendering) + else space, (snd rendering) in renderings := rendering' :: !renderings; - let bonus = if use_indent then indent_bonus else spacing_bonus in rem_space := !rem_space - (space + bonus) in let end_cluster () = - let new_rows = merge_columns sep (List.rev !renderings) in + let new_len, new_rows = merge_columns sep (List.rev !renderings) in rows := List.rev_append new_rows !rows; + max_len := max !max_len new_len; rem_space := size - indent_bonus; renderings := []; first_row := false @@ -214,7 +221,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = end) fs; if !renderings <> [] then end_cluster (); - max_len !rows, List.rev !rows) + !max_len, List.rev !rows) in snd (aux_box markup size) -- 2.39.2