1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
29 (** {2 Pretty printing from BoxML to strings} *)
31 let utf8_string_length s = Utf8.compute_len s 0 (String.length s)
33 let string_space = " "
34 let string_space_len = utf8_string_length string_space
35 let string_indent = (* string_space *) ""
36 let string_indent_len = utf8_string_length string_indent
37 let string_ink = "---------------------------"
38 let string_ink_len = utf8_string_length string_ink
40 let contains_attrs contained container =
41 List.for_all (fun attr -> List.mem attr container) contained
43 let want_indent = contains_attrs (RenderingAttrs.indent_attributes `BoxML)
44 let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML)
46 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
48 let indent_string s = string_indent ^ s
50 let indent_children (size, children) =
51 let children' = List.map indent_string children in
52 size + string_space_len, children'
54 let choose_rendering size (best, other) =
55 let best_size, _ = best in
56 if size >= best_size then best else other
58 (* merge_columns [ X1 ; X3 ] returns X1
61 let merge_columns sep cols =
62 let sep_len = utf8_string_length sep in
64 let res_rows = ref [] in
65 let add_row ~continue row =
67 | last :: prev when continue ->
68 res_rows := (last ^ sep ^ row) :: prev;
69 indent := !indent + utf8_string_length last + sep_len
70 | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows;
76 add_row ~continue:true hd;
77 List.iter (add_row ~continue:false) tl
83 List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0
85 let render_row available_space spacing children =
86 let spacing_bonus = if spacing then string_space_len else 0 in
87 let rem_space = ref available_space in
88 let renderings = ref [] in
91 let occupied_space, rendering = f !rem_space in
92 renderings := rendering :: !renderings;
93 rem_space := !rem_space - (occupied_space + spacing_bonus))
95 let sep = if spacing then string_space else "" in
96 let rendering = merge_columns sep (List.rev !renderings) in
97 max_len rendering, rendering
99 let fixed_rendering s =
100 let s_len = utf8_string_length s in
103 let render_to_strings ~map_unicode_to_tex choose_action size markup =
104 let max_size = max_int in
107 | Box.Text (_, t) -> fixed_rendering t
108 | Box.Space _ -> fixed_rendering string_space
109 | Box.Ink _ -> fixed_rendering string_ink
110 | Box.Action (_, []) -> assert false
111 | Box.Action (_, l) -> aux_box (choose_action l)
112 | Box.Object (_, o) -> fixed_rendering o
113 | Box.H (attrs, children) ->
114 let spacing = want_spacing attrs in
115 let children' = List.map aux_box children in
116 (fun size -> render_row size spacing children')
117 | Box.HV (attrs, children) ->
118 let spacing = want_spacing attrs in
119 let children' = List.map aux_box children in
121 let (size', renderings) as res =
122 render_row max_size spacing children'
124 if size' <= size then (* children fit in a row *)
126 else (* break needed, re-render using a Box.V *)
127 aux_box (Box.V (attrs, children)) size)
128 | Box.V (attrs, []) -> assert false
129 | Box.V (attrs, [child]) -> aux_box child
130 | Box.V (attrs, hd :: tl) ->
131 let indent = want_indent attrs in
132 let hd_f = aux_box hd in
133 let tl_fs = List.map aux_box tl in
135 let hd_rendering = snd (hd_f size) in
137 max 0 (if indent then size - string_indent_len else size)
142 (* let indent_header = if indent then string_indent else "" in *)
143 snd (indent_children (f children_size)))
146 let rows = hd_rendering @ List.concat tl_renderings in
148 | Box.HOV (attrs, []) -> assert false
149 | Box.HOV (attrs, [child]) -> aux_box child
150 | Box.HOV (attrs, children) ->
151 let spacing = want_spacing attrs in
152 let indent = want_indent attrs in
153 let spacing_bonus = if spacing then string_space_len else 0 in
154 let indent_bonus = if indent then string_indent_len else 0 in
155 let sep = if spacing then string_space else "" in
156 let fs = List.map aux_box children in
159 let renderings = ref [] in
160 let rem_space = ref size in
161 let first_row = ref true in
162 let use_rendering (space, rendering) =
163 let use_indent = !renderings = [] && not !first_row in
165 if use_indent then List.map indent_string rendering
168 renderings := rendering' :: !renderings;
169 let bonus = if use_indent then indent_bonus else spacing_bonus in
170 rem_space := !rem_space - (space + bonus)
173 let new_rows = merge_columns sep (List.rev !renderings) in
174 rows := List.rev_append new_rows !rows;
175 rem_space := size - indent_bonus;
181 let (best_space, _) as best = f max_size in
182 if best_space <= !rem_space then
186 if best_space <= !rem_space then use_rendering best
187 else use_rendering (f size)
190 if !renderings <> [] then end_cluster ();
191 max_len !rows, List.rev !rows)
193 snd (aux_box markup size)
195 let render_to_string ~map_unicode_to_tex choose_action size markup =
197 (render_to_strings ~map_unicode_to_tex choose_action size markup)