]> matita.cs.unibo.it Git - helm.git/blob - components/content_pres/boxPp.ml
tagged 0.5.0-rc1
[helm.git] / components / content_pres / boxPp.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 module Pres = Mpresentation
29
30 (** {2 Pretty printing from BoxML to strings} *)
31
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
38
39 let contains_attrs contained container =
40   List.for_all (fun attr -> List.mem attr container) contained
41
42 let want_indent = contains_attrs (RenderingAttrs.indent_attributes `BoxML)
43 let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML)
44
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'
49
50 let choose_rendering size (best, other) =
51   let best_size, _ = best in
52   if size >= best_size then best else other
53
54 let merge_columns sep cols =
55   let sep_len = String.length sep in
56   let indent = ref 0 in
57   let res_rows = ref [] in
58   let add_row ~continue row =
59     match !res_rows with
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;
64   in
65   List.iter
66     (fun rows ->
67       match rows with
68       | hd :: tl ->
69           add_row ~continue:true hd;
70           List.iter (add_row ~continue:false) tl
71       | [] -> ())
72     cols;
73   List.rev !res_rows
74     
75 let max_len =
76   List.fold_left (fun max_size s -> max (String.length s) max_size) 0
77
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
82   List.iter
83     (fun f ->
84       let occupied_space, rendering = f !rem_space in
85       renderings := rendering :: !renderings;
86       rem_space := !rem_space - (occupied_space + spacing_bonus))
87     children;
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
91
92 let fixed_rendering s =
93   let s_len = String.length s in
94   (fun _ -> s_len, [s])
95
96 let render_to_strings ~map_unicode_to_tex choose_action size markup =
97   let max_size = max_int in
98   let rec aux_box =
99     function
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
113         (fun size ->
114           let (size', renderings) as res =
115             render_row max_size spacing children'
116           in
117           if size' <= size then (* children fit in a row *)
118             res
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
127         (fun size ->
128           let _, hd_rendering = hd_f size in
129           let children_size =
130             max 0 (if indent then size - string_indent_len else size)
131           in
132           let tl_renderings =
133             List.map
134               (fun f ->
135 (*                 let indent_header = if indent then string_indent else "" in *)
136                 snd (indent_children (f children_size)))
137               tl_fs
138           in
139           let rows = hd_rendering @ List.concat tl_renderings in
140           max_len rows, rows)
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
150         (fun size ->
151           let rows = ref [] 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
157             let rendering' =
158               if use_indent then List.map indent_string rendering
159               else rendering
160             in
161             renderings := rendering' :: !renderings;
162             let bonus = if use_indent then indent_bonus else spacing_bonus in
163             rem_space := !rem_space - (space + bonus)
164           in
165           let end_cluster () =
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;
169             renderings := [];
170             first_row := false
171           in
172           List.iter
173             (fun f ->
174               let (best_space, _) as best = f max_size in
175               if best_space <= !rem_space then
176                 use_rendering best
177               else begin
178                 end_cluster ();
179                 if best_space <= !rem_space then use_rendering best
180                 else use_rendering (f size)
181               end)
182             fs;
183           if !renderings <> [] then end_cluster ();
184           max_len !rows, List.rev !rows)
185   and aux_mpres =
186     let text s = Pres.Mtext ([], s) in
187     let mrow c = Pres.Mrow ([], c) in
188     function
189     | Pres.Mi (_, s)
190     | Pres.Mn (_, s)
191     | Pres.Mtext (_, s)
192     | Pres.Ms (_, s)
193     | Pres.Mgliph (_, s) -> fixed_rendering s
194     | Pres.Mo (_, s) ->
195         let s =
196           if map_unicode_to_tex then begin
197             if String.length s = 1 && Char.code s.[0] < 128 then
198               s
199             else
200               match Utf8Macro.tex_of_unicode s with
201               | Some s -> s ^ " "
202               | None -> " " ^ s ^ " "
203           end else
204             s
205         in
206         fixed_rendering s
207     | Pres.Mspace _ -> fixed_rendering string_space
208     | Pres.Mrow (attrs, children) ->
209         let children' = List.map aux_mpres children in
210         (fun size -> render_row size false children')
211     | Pres.Mfrac (_, m, n) ->
212         aux_mpres (mrow [ text "\\frac("; text ")"; text "("; n; text ")" ])
213     | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text "\\sqrt("; m; text ")" ])
214     | Pres.Mroot (_, r, i) ->
215         aux_mpres (mrow [
216           text "\\root("; i; text ")"; text "\\of("; r; text ")" ])
217     | Pres.Mstyle (_, m)
218     | Pres.Merror (_, m)
219     | Pres.Mpadded (_, m)
220     | Pres.Mphantom (_, m)
221     | Pres.Menclose (_, m) -> aux_mpres m
222     | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
223     | Pres.Maction (_, []) -> assert false
224     | Pres.Msub (_, m, n) ->
225         aux_mpres (mrow [ text "("; m; text ")\\sub("; n; text ")" ])
226     | Pres.Msup (_, m, n) ->
227         aux_mpres (mrow [ text "("; m; text ")\\sup("; n; text ")" ])
228     | Pres.Munder (_, m, n) ->
229         aux_mpres (mrow [ text "("; m; text ")\\below("; n; text ")" ])
230     | Pres.Mover (_, m, n) ->
231         aux_mpres (mrow [ text "("; m; text ")\\above("; n; text ")" ])
232     | Pres.Msubsup _
233     | Pres.Munderover _
234     | Pres.Mtable _ ->
235         prerr_endline
236           "MathML presentation element not yet available in concrete syntax";
237         assert false
238     | Pres.Maction (_, hd :: _) -> aux_mpres hd
239     | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
240   in
241   snd (aux_mpres markup size)
242
243 let render_to_string ~map_unicode_to_tex choose_action size markup =
244   String.concat "\n"
245     (render_to_strings ~map_unicode_to_tex choose_action size markup)
246