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 small_skip_attributes _ = [ None, "width", "0.5em" ]
45 let want_indent = contains_attrs [ None, "indent", "0.5em" ]
46 let want_spacing = contains_attrs [ None, "spacing", "0.5em" ]
48 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
50 let indent_string s = string_indent ^ s
52 let indent_children (size, children) =
53 let children' = List.map indent_string children in
54 size + string_space_len, children'
56 let choose_rendering size (best, other) =
57 let best_size, _ = best in
58 if size >= best_size then best else other
60 (* merge_columns [ X1 ; X3 ] returns X1
63 let merge_columns sep cols =
64 let sep_len = utf8_string_length sep in
66 let res_rows = ref [] in
67 let add_row ~continue row =
69 | last :: prev when continue ->
70 res_rows := (last ^ sep ^ row) :: prev;
71 indent := !indent + utf8_string_length last + sep_len
72 | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows;
78 add_row ~continue:true hd;
79 List.iter (add_row ~continue:false) tl
85 List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0
87 let render_row available_space spacing children =
88 let spacing_bonus = if spacing then string_space_len else 0 in
89 let rem_space = ref available_space in
90 let renderings = ref [] in
93 let occupied_space, rendering = f !rem_space in
94 renderings := rendering :: !renderings;
95 rem_space := !rem_space - (occupied_space + spacing_bonus))
97 let sep = if spacing then string_space else "" in
98 let rendering = merge_columns sep (List.rev !renderings) in
99 max_len rendering, rendering
101 let fixed_rendering s =
102 let s_len = utf8_string_length s in
105 let render_to_strings ~map_unicode_to_tex choose_action size markup =
106 prerr_endline ("render size is " ^ string_of_int size);
107 let max_size = max_int in
110 | Box.Text (_, t) -> fixed_rendering t
111 | Box.Space _ -> fixed_rendering string_space
112 | Box.Ink _ -> fixed_rendering string_ink
113 | Box.Action (_, []) -> assert false
114 | Box.Action (_, l) -> aux_box (choose_action l)
115 | Box.Object (_, o) -> fixed_rendering o
116 | Box.H (attrs, children) ->
117 let spacing = want_spacing attrs in
118 let children' = List.map aux_box children in
119 (fun size -> render_row size spacing children')
120 | Box.HV (attrs, children) ->
121 let spacing = want_spacing attrs in
122 let children' = List.map aux_box children in
124 let (size', renderings) as res =
125 render_row max_size spacing children'
127 if size' <= size then (* children fit in a row *)
129 else (* break needed, re-render using a Box.V *)
130 aux_box (Box.V (attrs, children)) size)
131 | Box.V (attrs, []) -> aux_box (Box.Text (attrs,"")) (* FIXME *)
132 | Box.V (attrs, [child]) -> aux_box child
133 | Box.V (attrs, hd :: tl) ->
134 let indent = want_indent attrs in
135 let hd_f = aux_box hd in
136 let tl_fs = List.map aux_box tl in
138 let hd_rendering = snd (hd_f size) in
140 max 0 (if indent then size - string_indent_len else size)
145 (* let indent_header = if indent then string_indent else "" in *)
146 snd (indent_children (f children_size)))
149 let rows = hd_rendering @ List.concat tl_renderings in
151 | Box.HOV (attrs, []) -> assert false
152 | Box.HOV (attrs, [child]) -> aux_box child
153 | Box.HOV (attrs, children) ->
154 let spacing = want_spacing attrs in
155 let indent = want_indent attrs in
156 let spacing_bonus = if spacing then string_space_len else 0 in
157 let indent_bonus = if indent then string_indent_len else 0 in
158 let sep = if spacing then string_space else "" in
159 let fs = List.map aux_box children in
162 let renderings = ref [] in
163 let rem_space = ref size in
164 let first_row = ref true in
165 let use_rendering (space, rendering) =
166 let use_indent = !renderings = [] && not !first_row in
168 if use_indent then List.map indent_string rendering
171 renderings := rendering' :: !renderings;
172 let bonus = if use_indent then indent_bonus else spacing_bonus in
173 rem_space := !rem_space - (space + bonus)
176 let new_rows = merge_columns sep (List.rev !renderings) in
177 rows := List.rev_append new_rows !rows;
178 rem_space := size - indent_bonus;
184 let (best_space, _) as best = f max_size in
185 if best_space <= !rem_space then
189 if best_space <= !rem_space then use_rendering best
190 else use_rendering (f size)
193 if !renderings <> [] then end_cluster ();
194 max_len !rows, List.rev !rows)
196 snd (aux_box markup size)
198 let render_to_string ~map_unicode_to_tex choose_action size markup =
200 (render_to_strings ~map_unicode_to_tex choose_action size markup)