]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/content_pres/boxPp.ml
9511de631380c8b72d4bff00cca1500c3fa8b79a
[helm.git] / matitaB / 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
29 (** {2 Pretty printing from BoxML to strings} *)
30
31 let utf8_string_length s = Utf8.compute_len s 0 (String.length s)
32
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
39
40 let contains_attrs contained container =
41   List.for_all (fun attr -> List.mem attr container) contained
42
43 let small_skip_attributes _ = [ None, "width", "0.5em" ]
44
45 let want_indent = contains_attrs [ None, "indent", "0.5em" ]
46 let want_spacing = contains_attrs [ None, "spacing", "0.5em" ]
47
48 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
49
50 let indent_string s = string_indent ^ s
51
52 let indent_children (size, children) =
53   let children' = List.map indent_string children in
54   size + string_space_len, children'
55
56 let choose_rendering size (best, other) =
57   let best_size, _ = best in
58   if size >= best_size then best else other
59
60 (* merge_columns [ X1 ;  X3 ] returns X1
61                    X2    X4           X2 X3
62                                          X4 *)
63 let merge_columns sep cols =
64   let sep_len = utf8_string_length sep in
65   let indent = ref 0 in
66   let res_rows = ref [] in
67   let add_row ~continue row =
68     match !res_rows with
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;
73   in
74   List.iter
75     (fun rows ->
76       match rows with
77       | hd :: tl ->
78           add_row ~continue:true hd;
79           List.iter (add_row ~continue:false) tl
80       | [] -> ())
81     cols;
82   List.rev !res_rows
83     
84 let max_len =
85   List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0
86
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
91   List.iter
92     (fun f ->
93       let occupied_space, rendering = f !rem_space in
94       renderings := rendering :: !renderings;
95       rem_space := !rem_space - (occupied_space + spacing_bonus))
96     children;
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
100
101 let fixed_rendering s = 
102   let s_len = utf8_string_length s in
103   fun _ -> s_len,[s]
104
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
108   let rec aux_box =
109     function
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
123         (fun size ->
124           let (size', renderings) as res =
125             render_row max_size spacing children'
126           in
127           if size' <= size then (* children fit in a row *)
128             res
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
137         (fun size ->
138           let hd_rendering = snd (hd_f size) in
139           let children_size =
140             max 0 (if indent then size - string_indent_len else size)
141           in
142           let tl_renderings =
143             List.map
144               (fun f ->
145 (*                 let indent_header = if indent then string_indent else "" in *)
146                 snd (indent_children (f children_size)))
147               tl_fs
148           in
149           let rows = hd_rendering @ List.concat tl_renderings in
150           max_len rows, rows)
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
160         (fun size ->
161           let rows = ref [] 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
167             let rendering' =
168               if use_indent then List.map indent_string rendering
169               else rendering
170             in
171             renderings := rendering' :: !renderings;
172             let bonus = if use_indent then indent_bonus else spacing_bonus in
173             rem_space := !rem_space - (space + bonus)
174           in
175           let end_cluster () =
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;
179             renderings := [];
180             first_row := false
181           in
182           List.iter
183             (fun f ->
184               let (best_space, _) as best = f max_size in
185               if best_space <= !rem_space then
186                 use_rendering best
187               else begin
188                 end_cluster ();
189                 if best_space <= !rem_space then use_rendering best
190                 else use_rendering (f size)
191               end)
192             fs;
193           if !renderings <> [] then end_cluster ();
194           max_len !rows, List.rev !rows)
195   in
196   snd (aux_box markup size)
197
198 let render_to_string ~map_unicode_to_tex choose_action size markup =
199  String.concat "\n"
200   (render_to_strings ~map_unicode_to_tex choose_action size markup)