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 want_indent = contains_attrs (* (RenderingAttrs.indent_attributes `BoxML) *)[]
  44 let want_spacing = contains_attrs (* (RenderingAttrs.spacing_attributes `BoxML) *) []
  45
  46 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
  47
  48 let indent_string s = string_indent ^ s
  49
  50 let indent_children (size, children) =
  51   let children' = List.map indent_string children in
  52   size + string_space_len, children'
  53
  54 let choose_rendering size (best, other) =
  55   let best_size, _ = best in
  56   if size >= best_size then best else other
  57
  58 (* merge_columns [ X1 ;  X3 ] returns X1
  59                    X2    X4           X2 X3
  60                                          X4 *)
  61 let merge_columns sep cols =
  62   let sep_len = utf8_string_length sep in
  63   let indent = ref 0 in
  64   let res_rows = ref [] in
  65   let add_row ~continue row =
  66     match !res_rows with
  67     | last :: prev when continue ->
  68         res_rows := (last ^ sep ^ row) :: prev;
  69         indent := !indent + utf8_string_length last + sep_len
  70     | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows;
  71   in
  72   List.iter
  73     (fun rows ->
  74       match rows with
  75       | hd :: tl ->
  76           add_row ~continue:true hd;
  77           List.iter (add_row ~continue:false) tl
  78       | [] -> ())
  79     cols;
  80   List.rev !res_rows
  81
  82 let max_len =
  83   List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0
  84
  85 let render_row available_space spacing children =
  86   let spacing_bonus = if spacing then string_space_len else 0 in
  87   let rem_space = ref available_space in
  88   let renderings = ref [] in
  89   List.iter
  90     (fun f ->
  91       let occupied_space, rendering = f !rem_space in
  92       renderings := rendering :: !renderings;
  93       rem_space := !rem_space - (occupied_space + spacing_bonus))
  94     children;
  95   let sep = if spacing then string_space else "" in
  96   let rendering = merge_columns sep (List.rev !renderings) in
  97   max_len rendering, rendering
  98
  99 let fixed_rendering s =
 100   let s_len = utf8_string_length s in
 101   fun _ -> s_len,[s]
 102
 103 let render_to_strings ~map_unicode_to_tex choose_action size markup =
 104   prerr_endline ("render size is " ^ string_of_int size);
 105   let max_size = max_int in
 106   let rec aux_box =
 107     function
 108     | Box.Text (_, t) -> fixed_rendering t
 109     | Box.Space _ -> fixed_rendering string_space
 110     | Box.Ink _ -> fixed_rendering string_ink
 111     | Box.Action (_, []) -> assert false
 112     | Box.Action (_, l) -> aux_box (choose_action l)
 113     | Box.Object (_, o) -> fixed_rendering o
 114     | Box.H (attrs, children) ->
 115         let spacing = want_spacing attrs in
 116         let children' = List.map aux_box children in
 117         (fun size -> render_row size spacing children')
 118     | Box.HV (attrs, children) ->
 119         let spacing = want_spacing attrs in
 120         let children' = List.map aux_box children in
 121         (fun size ->
 122           let (size', renderings) as res =
 123             render_row max_size spacing children'
 124           in
 125           if size' <= size then (* children fit in a row *)
 126             res
 127           else  (* break needed, re-render using a Box.V *)
 128             aux_box (Box.V (attrs, children)) size)
 129     | Box.V (attrs, []) -> aux_box (Box.Text (attrs,"")) (* FIXME *)
 130     | Box.V (attrs, [child]) -> aux_box child
 131     | Box.V (attrs, hd :: tl) ->
 132         let indent = want_indent attrs in
 133         let hd_f = aux_box hd in
 134         let tl_fs = List.map aux_box tl in
 135         (fun size ->
 136           let hd_rendering = snd (hd_f size) in
 137           let children_size =
 138             max 0 (if indent then size - string_indent_len else size)
 139           in
 140           let tl_renderings =
 141             List.map
 142               (fun f ->
 143 (*                 let indent_header = if indent then string_indent else "" in *)
 144                 snd (indent_children (f children_size)))
 145               tl_fs
 146           in
 147           let rows = hd_rendering @ List.concat tl_renderings in
 148           max_len rows, rows)
 149     | Box.HOV (attrs, []) -> assert false
 150     | Box.HOV (attrs, [child]) -> aux_box child
 151     | Box.HOV (attrs, children) ->
 152         let spacing = want_spacing attrs in
 153         let indent = want_indent attrs in
 154         let spacing_bonus = if spacing then string_space_len else 0 in
 155         let indent_bonus = if indent then string_indent_len else 0 in
 156         let sep = if spacing then string_space else "" in
 157         let fs = List.map aux_box children in
 158         (fun size ->
 159           let rows = ref [] in
 160           let renderings = ref [] in
 161           let rem_space = ref size in
 162           let first_row = ref true in
 163           let use_rendering (space, rendering) =
 164             let use_indent = !renderings = [] && not !first_row in
 165             let rendering' =
 166               if use_indent then List.map indent_string rendering
 167               else rendering
 168             in
 169             renderings := rendering' :: !renderings;
 170             let bonus = if use_indent then indent_bonus else spacing_bonus in
 171             rem_space := !rem_space - (space + bonus)
 172           in
 173           let end_cluster () =
 174             let new_rows = merge_columns sep (List.rev !renderings) in
 175             rows := List.rev_append new_rows !rows;
 176             rem_space := size - indent_bonus;
 177             renderings := [];
 178             first_row := false
 179           in
 180           List.iter
 181             (fun f ->
 182               let (best_space, _) as best = f max_size in
 183               if best_space <= !rem_space then
 184                 use_rendering best
 185               else begin
 186                 end_cluster ();
 187                 if best_space <= !rem_space then use_rendering best
 188                 else use_rendering (f size)
 189               end)
 190             fs;
 191           if !renderings <> [] then end_cluster ();
 192           max_len !rows, List.rev !rows)
 193   in
 194   snd (aux_box markup size)
 195
 196 let render_to_string ~map_unicode_to_tex choose_action size markup =
 197  String.concat "\n"
 198   (render_to_strings ~map_unicode_to_tex choose_action size markup)