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/
26 module Pres = Mpresentation
28 (** {2 Pretty printing from BoxML to strings} *)
30 let string_space = " "
31 let string_space_len = String.length string_space
32 let string_indent = string_space
33 let string_indent_len = String.length string_indent
35 let string_ink_len = String.length string_ink
37 let contains_attrs contained container =
38 List.for_all (fun attr -> List.mem attr container) contained
40 let want_indent = contains_attrs (RenderingAttrs.indent_attributes `BoxML)
41 let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML)
43 let indent_string s = string_indent ^ s
44 let indent_children (size, children) =
45 let children' = List.map indent_string children in
46 size + string_space_len, children'
48 let choose_rendering size (best, other) =
49 let best_size, _ = best in
50 if size >= best_size then best else other
52 let merge_columns sep cols =
53 let sep_len = String.length sep in
55 let res_rows = ref [] in
56 let add_row ~continue row =
58 | last :: prev when continue ->
59 res_rows := (String.concat sep [last; row]) :: prev;
60 indent := !indent + String.length last + sep_len
61 | _ -> res_rows := (String.make !indent ' ' ^ row) :: !res_rows;
67 add_row ~continue:true hd;
68 List.iter (add_row ~continue:false) tl
74 List.fold_left (fun max_size s -> max (String.length s) max_size) 0
76 let render_row available_space spacing children =
77 let spacing_bonus = if spacing then string_space_len else 0 in
78 let rem_space = ref available_space in
79 let renderings = ref [] in
82 let occupied_space, rendering = f !rem_space in
83 renderings := rendering :: !renderings;
84 rem_space := !rem_space - (occupied_space + spacing_bonus))
86 let sep = if spacing then string_space else "" in
87 let rendering = merge_columns sep (List.rev !renderings) in
88 max_len rendering, rendering
90 let fixed_rendering s =
91 let s_len = String.length s in
94 let render_to_strings size markup =
95 let max_size = max_int in
98 | Box.Text (_, t) -> fixed_rendering t
99 | Box.Space _ -> fixed_rendering string_space
100 | Box.Ink _ -> fixed_rendering string_ink
101 | Box.Action (_, []) -> assert false
102 | Box.Action (_, hd :: _) -> aux_box hd
103 | Box.Object (_, o) -> aux_mpres o
104 | Box.H (attrs, children) ->
105 let spacing = want_spacing attrs in
106 let children' = List.map aux_box children in
107 (fun size -> render_row size spacing children')
108 | Box.HV (attrs, children) ->
109 let spacing = want_spacing attrs in
110 let children' = List.map aux_box children in
112 let (size', renderings) as res =
113 render_row max_size spacing children'
115 if size' <= size then (* children fit in a row *)
117 else (* break needed, re-render using a Box.V *)
118 aux_box (Box.V (attrs, children)) size)
119 | Box.V (attrs, []) -> assert false
120 | Box.V (attrs, [child]) -> aux_box child
121 | Box.V (attrs, hd :: tl) ->
122 let indent = want_indent attrs in
123 let hd_f = aux_box hd in
124 let tl_fs = List.map aux_box tl in
126 let _, hd_rendering = hd_f size in
128 max 0 (if indent then size - string_indent_len else size)
133 let indent_header = if indent then string_indent else "" in
134 snd (indent_children (f children_size)))
137 let rows = hd_rendering @ List.concat tl_renderings in
139 | Box.HOV (attrs, []) -> assert false
140 | Box.HOV (attrs, [child]) -> aux_box child
141 | Box.HOV (attrs, children) ->
142 let spacing = want_spacing attrs in
143 let indent = want_indent attrs in
144 let spacing_bonus = if spacing then string_space_len else 0 in
145 let indent_bonus = if indent then string_indent_len else 0 in
146 let sep = if spacing then string_space else "" in
147 let fs = List.map aux_box children in
150 let renderings = ref [] in
151 let rem_space = ref size in
152 let first_row = ref true in
153 let use_rendering (space, rendering) =
154 let use_indent = !renderings = [] && not !first_row in
156 if use_indent then List.map indent_string rendering
159 renderings := rendering' :: !renderings;
160 let bonus = if use_indent then indent_bonus else spacing_bonus in
161 rem_space := !rem_space - (space + bonus)
164 let new_rows = merge_columns sep (List.rev !renderings) in
165 rows := List.rev_append new_rows !rows;
166 rem_space := size - indent_bonus;
172 let (best_space, _) as best = f max_size in
173 if best_space <= !rem_space then
177 if best_space <= !rem_space then use_rendering best
178 else use_rendering (f size)
181 if !renderings <> [] then end_cluster ();
182 max_len !rows, List.rev !rows)
184 let text s = Pres.Mtext ([], s) in
185 let mrow c = Pres.Mrow ([], c) in
191 | Pres.Mgliph (_, s) -> fixed_rendering s
194 if String.length s > 1 then
195 (* heuristic to guess which operators need to be expanded in their
197 Utf8Macro.tex_of_unicode s ^ " "
201 | Pres.Mspace _ -> fixed_rendering string_space
202 | Pres.Mrow (attrs, children) ->
203 let children' = List.map aux_mpres children in
204 (fun size -> render_row size false children')
205 | Pres.Mfrac (_, m, n) ->
206 aux_mpres (mrow [ text "\\frac("; text ")"; text "("; n; text ")" ])
207 | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text "\\sqrt("; m; text ")" ])
208 | Pres.Mroot (_, r, i) ->
210 text "\\root("; i; text ")"; text "\\of("; r; text ")" ])
213 | Pres.Mpadded (_, m)
214 | Pres.Mphantom (_, m)
215 | Pres.Menclose (_, m) -> aux_mpres m
216 | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
217 | Pres.Maction (_, []) -> assert false
218 | Pres.Msub (_, m, n) ->
219 aux_mpres (mrow [ text "("; m; text ")\\sub("; n; text ")" ])
220 | Pres.Msup (_, m, n) ->
221 aux_mpres (mrow [ text "("; m; text ")\\sup("; n; text ")" ])
222 | Pres.Munder (_, m, n) ->
223 aux_mpres (mrow [ text "("; m; text ")\\below("; n; text ")" ])
224 | Pres.Mover (_, m, n) ->
225 aux_mpres (mrow [ text "("; m; text ")\\above("; n; text ")" ])
230 "MathML presentation element not yet available in concrete syntax";
232 | Pres.Maction (_, hd :: _) -> aux_mpres hd
233 | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
235 snd (aux_mpres markup size)
237 let render_to_string size markup =
238 String.concat "\n" (render_to_strings size markup)