matita/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 (* merge_columns [ X1 ;  X3 ] returns X1
  55                    X2    X4           X2 X3
  56                                          X4 *)
  57 let merge_columns sep cols =
  58   let sep_len = String.length sep in
  59   let indent = ref 0 in
  60   let res_rows = ref [] in
  61   let add_row ~continue row =
  62     match !res_rows with
  63     | last :: prev when continue ->
  64         res_rows := (String.concat sep [last; row]) :: prev;
  65         indent := !indent + String.length last + sep_len
  66     | _ -> res_rows := (String.make !indent ' ' ^ row) :: !res_rows;
  67   in
  68   List.iter
  69     (fun rows ->
  70       match rows with
  71       | hd :: tl ->
  72           add_row ~continue:true hd;
  73           List.iter (add_row ~continue:false) tl
  74       | [] -> ())
  75     cols;
  76   List.rev !res_rows
  77
  78 let max_len =
  79   List.fold_left (fun max_size s -> max (String.length s) max_size) 0
  80
  81 let render_row available_space spacing children =
  82   let spacing_bonus = if spacing then string_space_len else 0 in
  83   let rem_space = ref available_space in
  84   let renderings = ref [] in
  85   List.iter
  86     (fun f ->
  87       let occupied_space, rendering = f !rem_space in
  88       renderings := rendering :: !renderings;
  89       rem_space := !rem_space - (occupied_space + spacing_bonus))
  90     children;
  91   let sep = if spacing then string_space else "" in
  92   let rendering = merge_columns sep (List.rev !renderings) in
  93   max_len rendering, rendering
  94
  95 let fixed_rendering s =
  96   let s_len = String.length s in
  97   (fun _ -> s_len, [s])
  98
  99 let render_to_strings ~map_unicode_to_tex choose_action size markup =
 100   let max_size = max_int in
 101   let rec aux_box =
 102     function
 103     | Box.Text (_, t) -> fixed_rendering t
 104     | Box.Space _ -> fixed_rendering string_space
 105     | Box.Ink _ -> fixed_rendering string_ink
 106     | Box.Action (_, []) -> assert false
 107     | Box.Action (_, l) -> aux_box (choose_action l)
 108     | Box.Object (_, o) -> aux_mpres o
 109     | Box.H (attrs, children) ->
 110         let spacing = want_spacing attrs in
 111         let children' = List.map aux_box children in
 112         (fun size -> render_row size spacing children')
 113     | Box.HV (attrs, children) ->
 114         let spacing = want_spacing attrs in
 115         let children' = List.map aux_box children in
 116         (fun size ->
 117           let (size', renderings) as res =
 118             render_row max_size spacing children'
 119           in
 120           if size' <= size then (* children fit in a row *)
 121             res
 122           else  (* break needed, re-render using a Box.V *)
 123             aux_box (Box.V (attrs, children)) size)
 124     | Box.V (attrs, []) -> assert false
 125     | Box.V (attrs, [child]) -> aux_box child
 126     | Box.V (attrs, hd :: tl) ->
 127         let indent = want_indent attrs in
 128         let hd_f = aux_box hd in
 129         let tl_fs = List.map aux_box tl in
 130         (fun size ->
 131           let _, hd_rendering = hd_f size in
 132           let children_size =
 133             max 0 (if indent then size - string_indent_len else size)
 134           in
 135           let tl_renderings =
 136             List.map
 137               (fun f ->
 138 (*                 let indent_header = if indent then string_indent else "" in *)
 139                 snd (indent_children (f children_size)))
 140               tl_fs
 141           in
 142           let rows = hd_rendering @ List.concat tl_renderings in
 143           max_len rows, rows)
 144     | Box.HOV (attrs, []) -> assert false
 145     | Box.HOV (attrs, [child]) -> aux_box child
 146     | Box.HOV (attrs, children) ->
 147         let spacing = want_spacing attrs in
 148         let indent = want_indent attrs in
 149         let spacing_bonus = if spacing then string_space_len else 0 in
 150         let indent_bonus = if indent then string_indent_len else 0 in
 151         let sep = if spacing then string_space else "" in
 152         let fs = List.map aux_box children in
 153         (fun size ->
 154           let rows = ref [] in
 155           let renderings = ref [] in
 156           let rem_space = ref size in
 157           let first_row = ref true in
 158           let use_rendering (space, rendering) =
 159             let use_indent = !renderings = [] && not !first_row in
 160             let rendering' =
 161               if use_indent then List.map indent_string rendering
 162               else rendering
 163             in
 164             renderings := rendering' :: !renderings;
 165             let bonus = if use_indent then indent_bonus else spacing_bonus in
 166             rem_space := !rem_space - (space + bonus)
 167           in
 168           let end_cluster () =
 169             let new_rows = merge_columns sep (List.rev !renderings) in
 170             rows := List.rev_append new_rows !rows;
 171             rem_space := size - indent_bonus;
 172             renderings := [];
 173             first_row := false
 174           in
 175           List.iter
 176             (fun f ->
 177               let (best_space, _) as best = f max_size in
 178               if best_space <= !rem_space then
 179                 use_rendering best
 180               else begin
 181                 end_cluster ();
 182                 if best_space <= !rem_space then use_rendering best
 183                 else use_rendering (f size)
 184               end)
 185             fs;
 186           if !renderings <> [] then end_cluster ();
 187           max_len !rows, List.rev !rows)
 188   and aux_mpres =
 189     let text s = Pres.Mtext ([], s) in
 190     let mrow c = Pres.Mrow ([], c) in
 191     let parentesize s = s in
 192     function
 193     | Pres.Mi (_, s)
 194     | Pres.Mn (_, s)
 195     | Pres.Mtext (_, s)
 196     | Pres.Ms (_, s)
 197     | Pres.Mgliph (_, s) -> fixed_rendering s
 198     | Pres.Mo (_, s) ->
 199         let s =
 200           if map_unicode_to_tex then begin
 201             if String.length s = 1 && Char.code s.[0] < 128 then
 202               s
 203             else
 204               match Utf8Macro.tex_of_unicode s with
 205               | s::_ -> s ^ " "
 206               | [] -> " " ^ s ^ " "
 207           end else
 208             s
 209         in
 210         fixed_rendering s
 211     | Pres.Mspace _ -> fixed_rendering string_space
 212     | Pres.Mrow (attrs, children) ->
 213         let children' = List.map aux_mpres children in
 214         (fun size -> render_row size false children')
 215     | Pres.Mfrac (_, m, n) ->
 216        aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ])
 217     | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "])
 218     | Pres.Mroot (_, r, i) ->
 219         aux_mpres (mrow [
 220           text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ])
 221     | Pres.Mstyle (_, m)
 222     | Pres.Merror (_, m)
 223     | Pres.Mpadded (_, m)
 224     | Pres.Mphantom (_, m)
 225     | Pres.Menclose (_, m) -> aux_mpres m
 226     | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
 227     | Pres.Maction (_, []) -> assert false
 228     | Pres.Msub (_, m, n) ->
 229         aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ])
 230     | Pres.Msup (_, m, n) ->
 231         aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ])
 232     | Pres.Munder (_, m, n) ->
 233         aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ])
 234     | Pres.Mover (_, m, n) ->
 235         aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ])
 236     | Pres.Msubsup _
 237     | Pres.Munderover _
 238     | Pres.Mtable _ ->
 239         prerr_endline
 240           "MathML presentation element not yet available in concrete syntax";
 241         assert false
 242     | Pres.Maction (_, hd :: _) -> aux_mpres hd
 243     | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup)
 244   in
 245   snd (aux_mpres markup size)
 246
 247 let render_to_string ~map_unicode_to_tex choose_action size markup =
 248  (* CSC: no information about hyperlinks yet *)
 249  [],
 250   String.concat "\n"
 251     (render_to_strings ~map_unicode_to_tex choose_action size markup)
 252