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