helm/software/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     let parentesize s = s in
 189     function
 190     | Pres.Mi (_, s)
 191     | Pres.Mn (_, s)
 192     | Pres.Mtext (_, s)
 193     | Pres.Ms (_, s)
 194     | Pres.Mgliph (_, s) -> fixed_rendering s
 195     | Pres.Mo (_, s) ->
 196         let s =
 197           if map_unicode_to_tex then begin
 198             if String.length s = 1 && Char.code s.[0] < 128 then
 199               s
 200             else
 201               match Utf8Macro.tex_of_unicode s with
 202               | s::_ -> s ^ " "
 203               | [] -> " " ^ s ^ " "
 204           end else
 205             s
 206         in
 207         fixed_rendering s
 208     | Pres.Mspace _ -> fixed_rendering string_space
 209     | Pres.Mrow (attrs, children) ->
 210         let children' = List.map aux_mpres children in
 211         (fun size -> render_row size false children')
 212     | Pres.Mfrac (_, m, n) ->
 213        aux_mpres (mrow [ text " \\frac "; parentesize m ; parentesize n])
 214     | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; ])
 215     | Pres.Mroot (_, r, i) ->
 216         aux_mpres (mrow [
 217           text " \\root "; parentesize i; text " \\of "; parentesize r ])
 218     | Pres.Mstyle (_, m)
 219     | Pres.Merror (_, m)
 220     | Pres.Mpadded (_, m)
 221     | Pres.Mphantom (_, m)
 222     | Pres.Menclose (_, m) -> aux_mpres m
 223     | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
 224     | Pres.Maction (_, []) -> assert false
 225     | Pres.Msub (_, m, n) ->
 226         aux_mpres (mrow [ parentesize m; text " \\sub "; parentesize n ])
 227     | Pres.Msup (_, m, n) ->
 228         aux_mpres (mrow [ parentesize m; text " \\sup "; parentesize n ])
 229     | Pres.Munder (_, m, n) ->
 230         aux_mpres (mrow [ parentesize m; text " \\below "; parentesize n ])
 231     | Pres.Mover (_, m, n) ->
 232         aux_mpres (mrow [ parentesize m; text " \\above "; parentesize n ])
 233     | Pres.Msubsup _
 234     | Pres.Munderover _
 235     | Pres.Mtable _ ->
 236         prerr_endline
 237           "MathML presentation element not yet available in concrete syntax";
 238         assert false
 239     | Pres.Maction (_, hd :: _) -> aux_mpres hd
 240     | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
 241   in
 242   snd (aux_mpres markup size)
 243
 244 let render_to_string ~map_unicode_to_tex choose_action size markup =
 245   String.concat "\n"
 246     (render_to_strings ~map_unicode_to_tex choose_action size markup)
 247