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/
28 module Pres = Mpresentation
30 (** {2 Pretty printing from BoxML to strings} *)
32 let string_space = " "
33 let string_space_len = String.length string_space
34 let string_indent = string_space
35 let string_indent_len = String.length string_indent
37 let string_ink_len = String.length string_ink
39 let contains_attrs contained container =
40 List.for_all (fun attr -> List.mem attr container) contained
42 let want_indent = contains_attrs (RenderingAttrs.indent_attributes `BoxML)
43 let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML)
45 let indent_string s = string_indent ^ s
46 let indent_children (size, children) =
47 let children' = List.map indent_string children in
48 size + string_space_len, children'
50 let choose_rendering size (best, other) =
51 let best_size, _ = best in
52 if size >= best_size then best else other
54 let merge_columns sep cols =
55 let sep_len = String.length sep in
57 let res_rows = ref [] in
58 let add_row ~continue row =
60 | last :: prev when continue ->
61 res_rows := (String.concat sep [last; row]) :: prev;
62 indent := !indent + String.length last + sep_len
63 | _ -> res_rows := (String.make !indent ' ' ^ row) :: !res_rows;
69 add_row ~continue:true hd;
70 List.iter (add_row ~continue:false) tl
76 List.fold_left (fun max_size s -> max (String.length s) max_size) 0
78 let render_row available_space spacing children =
79 let spacing_bonus = if spacing then string_space_len else 0 in
80 let rem_space = ref available_space in
81 let renderings = ref [] in
84 let occupied_space, rendering = f !rem_space in
85 renderings := rendering :: !renderings;
86 rem_space := !rem_space - (occupied_space + spacing_bonus))
88 let sep = if spacing then string_space else "" in
89 let rendering = merge_columns sep (List.rev !renderings) in
90 max_len rendering, rendering
92 let fixed_rendering s =
93 let s_len = String.length s in
96 let render_to_strings choose_action size markup =
97 let max_size = max_int in
100 | Box.Text (_, t) -> fixed_rendering t
101 | Box.Space _ -> fixed_rendering string_space
102 | Box.Ink _ -> fixed_rendering string_ink
103 | Box.Action (_, []) -> assert false
104 | Box.Action (_, l) -> aux_box (choose_action l)
105 | Box.Object (_, o) -> aux_mpres o
106 | Box.H (attrs, children) ->
107 let spacing = want_spacing attrs in
108 let children' = List.map aux_box children in
109 (fun size -> render_row size spacing children')
110 | Box.HV (attrs, children) ->
111 let spacing = want_spacing attrs in
112 let children' = List.map aux_box children in
114 let (size', renderings) as res =
115 render_row max_size spacing children'
117 if size' <= size then (* children fit in a row *)
119 else (* break needed, re-render using a Box.V *)
120 aux_box (Box.V (attrs, children)) size)
121 | Box.V (attrs, []) -> assert false
122 | Box.V (attrs, [child]) -> aux_box child
123 | Box.V (attrs, hd :: tl) ->
124 let indent = want_indent attrs in
125 let hd_f = aux_box hd in
126 let tl_fs = List.map aux_box tl in
128 let _, hd_rendering = hd_f size in
130 max 0 (if indent then size - string_indent_len else size)
135 (* let indent_header = if indent then string_indent else "" in *)
136 snd (indent_children (f children_size)))
139 let rows = hd_rendering @ List.concat tl_renderings in
141 | Box.HOV (attrs, []) -> assert false
142 | Box.HOV (attrs, [child]) -> aux_box child
143 | Box.HOV (attrs, children) ->
144 let spacing = want_spacing attrs in
145 let indent = want_indent attrs in
146 let spacing_bonus = if spacing then string_space_len else 0 in
147 let indent_bonus = if indent then string_indent_len else 0 in
148 let sep = if spacing then string_space else "" in
149 let fs = List.map aux_box children in
152 let renderings = ref [] in
153 let rem_space = ref size in
154 let first_row = ref true in
155 let use_rendering (space, rendering) =
156 let use_indent = !renderings = [] && not !first_row in
158 if use_indent then List.map indent_string rendering
161 renderings := rendering' :: !renderings;
162 let bonus = if use_indent then indent_bonus else spacing_bonus in
163 rem_space := !rem_space - (space + bonus)
166 let new_rows = merge_columns sep (List.rev !renderings) in
167 rows := List.rev_append new_rows !rows;
168 rem_space := size - indent_bonus;
174 let (best_space, _) as best = f max_size in
175 if best_space <= !rem_space then
179 if best_space <= !rem_space then use_rendering best
180 else use_rendering (f size)
183 if !renderings <> [] then end_cluster ();
184 max_len !rows, List.rev !rows)
186 let text s = Pres.Mtext ([], s) in
187 let mrow c = Pres.Mrow ([], c) in
193 | Pres.Mgliph (_, s) -> fixed_rendering s
196 if String.length s > 1 then
197 (* heuristic to guess which operators need to be expanded in their
199 Utf8Macro.tex_of_unicode s ^ " "
203 | Pres.Mspace _ -> fixed_rendering string_space
204 | Pres.Mrow (attrs, children) ->
205 let children' = List.map aux_mpres children in
206 (fun size -> render_row size false children')
207 | Pres.Mfrac (_, m, n) ->
208 aux_mpres (mrow [ text "\\frac("; text ")"; text "("; n; text ")" ])
209 | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text "\\sqrt("; m; text ")" ])
210 | Pres.Mroot (_, r, i) ->
212 text "\\root("; i; text ")"; text "\\of("; r; text ")" ])
215 | Pres.Mpadded (_, m)
216 | Pres.Mphantom (_, m)
217 | Pres.Menclose (_, m) -> aux_mpres m
218 | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
219 | Pres.Maction (_, []) -> assert false
220 | Pres.Msub (_, m, n) ->
221 aux_mpres (mrow [ text "("; m; text ")\\sub("; n; text ")" ])
222 | Pres.Msup (_, m, n) ->
223 aux_mpres (mrow [ text "("; m; text ")\\sup("; n; text ")" ])
224 | Pres.Munder (_, m, n) ->
225 aux_mpres (mrow [ text "("; m; text ")\\below("; n; text ")" ])
226 | Pres.Mover (_, m, n) ->
227 aux_mpres (mrow [ text "("; m; text ")\\above("; n; text ")" ])
232 "MathML presentation element not yet available in concrete syntax";
234 | Pres.Maction (_, hd :: _) -> aux_mpres hd
235 | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
237 snd (aux_mpres markup size)
239 let render_to_string choose_action size markup =
240 String.concat "\n" (render_to_strings choose_action size markup)