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
36 let string_ink = "---------------------------"
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 (* merge_columns [ X1 ; X3 ] returns X1
57 let merge_columns sep cols =
58 let sep_len = String.length sep in
60 let res_rows = ref [] in
61 let add_row ~continue row =
63 | last :: prev when continue ->
64 res_rows := (String.concat sep [last; row]) :: prev;
65 indent := !indent + String.length last + sep_len
66 | _ -> res_rows := (String.make !indent ' ' ^ row) :: !res_rows;
72 add_row ~continue:true hd;
73 List.iter (add_row ~continue:false) tl
79 List.fold_left (fun max_size s -> max (String.length s) max_size) 0
81 let render_row available_space spacing children =
82 let spacing_bonus = if spacing then string_space_len else 0 in
83 let rem_space = ref available_space in
84 let renderings = ref [] in
87 let occupied_space, rendering = f !rem_space in
88 renderings := rendering :: !renderings;
89 rem_space := !rem_space - (occupied_space + spacing_bonus))
91 let sep = if spacing then string_space else "" in
92 let rendering = merge_columns sep (List.rev !renderings) in
93 max_len rendering, rendering
95 let fixed_rendering s =
96 let s_len = String.length s in
99 let render_to_strings ~map_unicode_to_tex choose_action size markup =
100 let max_size = max_int in
103 | Box.Text (_, t) -> fixed_rendering t
104 | Box.Space _ -> fixed_rendering string_space
105 | Box.Ink _ -> fixed_rendering string_ink
106 | Box.Action (_, []) -> assert false
107 | Box.Action (_, l) -> aux_box (choose_action l)
108 | Box.Object (_, o) -> aux_mpres o
109 | Box.H (attrs, children) ->
110 let spacing = want_spacing attrs in
111 let children' = List.map aux_box children in
112 (fun size -> render_row size spacing children')
113 | Box.HV (attrs, children) ->
114 let spacing = want_spacing attrs in
115 let children' = List.map aux_box children in
117 let (size', renderings) as res =
118 render_row max_size spacing children'
120 if size' <= size then (* children fit in a row *)
122 else (* break needed, re-render using a Box.V *)
123 aux_box (Box.V (attrs, children)) size)
124 | Box.V (attrs, []) -> assert false
125 | Box.V (attrs, [child]) -> aux_box child
126 | Box.V (attrs, hd :: tl) ->
127 let indent = want_indent attrs in
128 let hd_f = aux_box hd in
129 let tl_fs = List.map aux_box tl in
131 let _, hd_rendering = hd_f size in
133 max 0 (if indent then size - string_indent_len else size)
138 (* let indent_header = if indent then string_indent else "" in *)
139 snd (indent_children (f children_size)))
142 let rows = hd_rendering @ List.concat tl_renderings in
144 | Box.HOV (attrs, []) -> assert false
145 | Box.HOV (attrs, [child]) -> aux_box child
146 | Box.HOV (attrs, children) ->
147 let spacing = want_spacing attrs in
148 let indent = want_indent attrs in
149 let spacing_bonus = if spacing then string_space_len else 0 in
150 let indent_bonus = if indent then string_indent_len else 0 in
151 let sep = if spacing then string_space else "" in
152 let fs = List.map aux_box children in
155 let renderings = ref [] in
156 let rem_space = ref size in
157 let first_row = ref true in
158 let use_rendering (space, rendering) =
159 let use_indent = !renderings = [] && not !first_row in
161 if use_indent then List.map indent_string rendering
164 renderings := rendering' :: !renderings;
165 let bonus = if use_indent then indent_bonus else spacing_bonus in
166 rem_space := !rem_space - (space + bonus)
169 let new_rows = merge_columns sep (List.rev !renderings) in
170 rows := List.rev_append new_rows !rows;
171 rem_space := size - indent_bonus;
177 let (best_space, _) as best = f max_size in
178 if best_space <= !rem_space then
182 if best_space <= !rem_space then use_rendering best
183 else use_rendering (f size)
186 if !renderings <> [] then end_cluster ();
187 max_len !rows, List.rev !rows)
189 let text s = Pres.Mtext ([], s) in
190 let mrow c = Pres.Mrow ([], c) in
191 let parentesize s = s in
197 | Pres.Mgliph (_, s) -> fixed_rendering s
200 if map_unicode_to_tex then begin
201 if String.length s = 1 && Char.code s.[0] < 128 then
204 match Utf8Macro.tex_of_unicode s with
206 | [] -> " " ^ s ^ " "
211 | Pres.Mspace _ -> fixed_rendering string_space
212 | Pres.Mrow (attrs, children) ->
213 let children' = List.map aux_mpres children in
214 (fun size -> render_row size false children')
215 | Pres.Mfrac (_, m, n) ->
216 aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ])
217 | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "])
218 | Pres.Mroot (_, r, i) ->
220 text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ])
223 | Pres.Mpadded (_, m)
224 | Pres.Mphantom (_, m)
225 | Pres.Menclose (_, m) -> aux_mpres m
226 | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
227 | Pres.Maction (_, []) -> assert false
228 | Pres.Msub (_, m, n) ->
229 aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ])
230 | Pres.Msup (_, m, n) ->
231 aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ])
232 | Pres.Munder (_, m, n) ->
233 aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ])
234 | Pres.Mover (_, m, n) ->
235 aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ])
240 "MathML presentation element not yet available in concrete syntax";
242 | Pres.Maction (_, hd :: _) -> aux_mpres hd
243 | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
245 snd (aux_mpres markup size)
247 let render_to_string ~map_unicode_to_tex choose_action size markup =
248 (* CSC: no information about hyperlinks yet *)
251 (render_to_strings ~map_unicode_to_tex choose_action size markup)