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 =
  32   Utf8.compute_len s 0 (String.length s)
  33
  34 let string_space = " "
  35 let string_space_len = utf8_string_length string_space
  36 let string_indent = (* string_space *) " "
  37 let string_indent_len = utf8_string_length string_indent
  38 let string_ink = "---------------------------"
  39 let string_ink_len = utf8_string_length string_ink
  40
  41 let contains_attrs contained container =
  42   List.for_all (fun attr -> List.mem attr container) contained
  43
  44 let small_skip_attributes _ = [ None, "width", "0.5em" ]
  45
  46 let want_indent = contains_attrs [ None, "indent", "0.5em" ]
  47 let want_spacing = contains_attrs [ None, "spacing", "0.5em" ]
  48
  49 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
  50
  51 let indent_string s = string_indent ^ s
  52
  53 let indent_children (size, children) =
  54   let children' = List.map indent_string children in
  55   size + string_space_len, children'
  56
  57 let choose_rendering size (best, other) =
  58   let best_size, _ = best in
  59   if size >= best_size then best else other
  60
  61 (* merge_columns [ X1 ;  X3 ] returns X1
  62                    X2    X4           X2 X3
  63                                          X4 *)
  64 let merge_columns sep cols =
  65   let sep_len = utf8_string_length sep in
  66   let indent = ref 0 in
  67   let res_rows = ref [] in
  68   let max_len = ref 0 in
  69   let add_row ~continue size row =
  70     match !res_rows with
  71     | last :: prev when continue ->
  72         res_rows := (last ^ sep ^ row) :: prev;
  73         indent := size
  74     | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows;
  75   in
  76   List.iter
  77     (fun (len,rows) ->
  78       (match rows with
  79       | hd :: tl ->
  80           add_row ~continue:true !max_len hd;
  81           List.iter (add_row ~continue:false len) tl
  82       | [] -> ());
  83       max_len := !max_len + len + sep_len)
  84     cols;
  85   !max_len, List.rev !res_rows
  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*) rendering = f !rem_space in
  94       let occupied_space,_ = rendering in
  95       renderings := rendering :: !renderings;
  96       rem_space := !rem_space - (occupied_space + spacing_bonus))
  97     children;
  98   let sep = if spacing then string_space else "" in
  99   (*let rendering = merge_columns sep (List.rev !renderings) in
 100   max_len rendering, rendering *)
 101   merge_columns sep (List.rev !renderings)
 102
 103 let fixed_rendering s =
 104   let s_len = utf8_string_length s in
 105   fun _ -> s_len,[s]
 106
 107 let render_to_strings ~map_unicode_to_tex choose_action size markup =
 108   prerr_endline ("render size is " ^ string_of_int size);
 109   let add_markup attr txt =
 110     let txt = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt in
 111     let value_of_attr (_,_,v) = v in
 112     let title =
 113       try Some (value_of_attr (List.find (fun (_,t,_) -> t = "title") attr))
 114       with _ -> None in
 115     let href =
 116       try Some (value_of_attr (List.find (fun (_,t,_) -> t = "href") attr))
 117       with _ -> None in
 118     match title,href with
 119     | None,None -> txt
 120     | None,Some u -> "<A href=\"" ^ u ^ "\">" ^ txt ^ "</A>"
 121     | Some t, Some u ->
 122        "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
 123     | Some t, None ->
 124        let u = "cic:/fakeuri.con" in
 125        "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
 126   in
 127
 128   let max_size = max_int in
 129   let rec aux_box =
 130     function
 131     | Box.Text (attr, t) ->
 132         fun x ->
 133         (match fixed_rendering t x with
 134          | len, [txt] -> len, [add_markup attr txt]
 135          | _ -> assert false)
 136     | Box.Space _ -> fixed_rendering string_space
 137     | Box.Ink _ -> fixed_rendering string_ink
 138     | Box.Action (_, []) -> assert false
 139     | Box.Action (_, l) -> aux_box (choose_action l)
 140     | Box.Object (_, o) -> fixed_rendering o
 141     | Box.H (attrs, children) ->
 142         let spacing = want_spacing attrs in
 143         let children' = List.map aux_box children in
 144         (fun size -> render_row size spacing children')
 145     | Box.HV (attrs, children) ->
 146         let spacing = want_spacing attrs in
 147         let children' = List.map aux_box children in
 148         (fun size ->
 149           let (size', renderings) as res =
 150             render_row max_size spacing children'
 151           in
 152           if size' <= size then (* children fit in a row *)
 153             res
 154           else  (* break needed, re-render using a Box.V *)
 155             aux_box (Box.V (attrs, children)) size)
 156     | Box.V (attrs, []) -> aux_box (Box.Text (attrs,"")) (* FIXME *)
 157     | Box.V (attrs, [child]) -> aux_box child
 158     | Box.V (attrs, hd :: tl) ->
 159         let indent = want_indent attrs in
 160         let hd_f = aux_box hd in
 161         let tl_fs = List.map aux_box tl in
 162         (fun size ->
 163           let hd_rendering = hd_f size in
 164           let children_size =
 165             max 0 (if indent then size - string_indent_len else size)
 166           in
 167           let tl_renderings =
 168             List.map
 169               (fun f ->
 170 (*                 let indent_header = if indent then string_indent else "" in *)
 171                 indent_children (f children_size))
 172               tl_fs
 173           in
 174             List.fold_right
 175               (fun (len,row) (acclen,accrows) -> max acclen len, row@accrows)
 176               (hd_rendering::tl_renderings) (0,[]))
 177     | Box.HOV (attrs, []) -> assert false
 178     | Box.HOV (attrs, [child]) -> aux_box child
 179     | Box.HOV (attrs, children) ->
 180         let spacing = want_spacing attrs in
 181         let indent = want_indent attrs in
 182         let spacing_bonus = if spacing then string_space_len else 0 in
 183         let indent_bonus = if indent then string_indent_len else 0 in
 184         let sep = if spacing then string_space else "" in
 185         let fs = List.map aux_box children in
 186         (fun size ->
 187           let rows = ref [] in
 188           let renderings = ref [] in
 189           let rem_space = ref size in
 190           let first_row = ref true in
 191           let max_len = ref 0 in
 192           let use_rendering (* (space, rendering) *) rendering =
 193             let space, _ = rendering in
 194             let use_indent = !renderings = [] && not !first_row in
 195             let bonus = if use_indent then indent_bonus else spacing_bonus in
 196             let rendering' = (* space+bonus, *)
 197               if use_indent then
 198                  space+indent_bonus, List.map indent_string (snd rendering)
 199               else space, (snd rendering)
 200             in
 201             renderings := rendering' :: !renderings;
 202             rem_space := !rem_space - (space + bonus)
 203           in
 204           let end_cluster () =
 205             let new_len, new_rows = merge_columns sep (List.rev !renderings) in
 206             rows := List.rev_append new_rows !rows;
 207             max_len := max !max_len new_len;
 208             rem_space := size - indent_bonus;
 209             renderings := [];
 210             first_row := false
 211           in
 212           List.iter
 213             (fun f ->
 214               let (best_space, _) as best = f max_size in
 215               if best_space <= !rem_space then
 216                 use_rendering best
 217               else begin
 218                 end_cluster ();
 219                 if best_space <= !rem_space then use_rendering best
 220                 else use_rendering (f size)
 221               end)
 222             fs;
 223           if !renderings <> [] then end_cluster ();
 224           !max_len, List.rev !rows)
 225   in
 226   snd (aux_box markup size)
 227
 228 let render_to_string ~map_unicode_to_tex choose_action size markup =
 229  String.concat "\n"
 230   (render_to_strings ~map_unicode_to_tex choose_action size markup)