(* Copyright (C) 2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* Department, University of Bologna, Italy.
*
* HELM is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* HELM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with HELM; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston,
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
* http://helm.cs.unibo.it/
*)
(* $Id$ *)
(** {2 Pretty printing from BoxML to strings} *)
let utf8_string_length s =
Utf8.compute_len s 0 (String.length s)
let string_space = " "
let string_space_len = utf8_string_length string_space
let string_indent = (* string_space *) " "
let string_indent_len = utf8_string_length string_indent
let string_ink = "---------------------------"
let string_ink_len = utf8_string_length string_ink
let contains_attrs contained container =
List.for_all (fun attr -> List.mem attr container) contained
let small_skip_attributes _ = [ None, "width", "0.5em" ]
let want_indent = contains_attrs [ None, "indent", "0.5em" ]
let want_spacing = contains_attrs [ None, "spacing", "0.5em" ]
let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
let indent_string s = string_indent ^ s
let indent_children (size, children) =
let children' = List.map indent_string children in
size + string_space_len, children'
let choose_rendering size (best, other) =
let best_size, _ = best in
if size >= best_size then best else other
(* merge_columns [ X1 ; X3 ] returns X1
X2 X4 X2 X3
X4 *)
let merge_columns sep cols =
let sep_len = utf8_string_length sep in
let indent = ref 0 in
let res_rows = ref [] in
let max_len = ref 0 in
let add_row ~continue size row =
match !res_rows with
| last :: prev when continue ->
res_rows := (last ^ sep ^ row) :: prev;
indent := size
| _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows;
in
List.iter
(fun (len,rows) ->
(match rows with
| hd :: tl ->
add_row ~continue:true !max_len hd;
List.iter (add_row ~continue:false len) tl
| [] -> ());
max_len := !max_len + len + sep_len)
cols;
!max_len, List.rev !res_rows
let render_row available_space spacing children =
let spacing_bonus = if spacing then string_space_len else 0 in
let rem_space = ref available_space in
let renderings = ref [] in
List.iter
(fun f ->
let (*occupied_space, rendering*) rendering = f !rem_space in
let occupied_space,_ = rendering in
renderings := rendering :: !renderings;
rem_space := !rem_space - (occupied_space + spacing_bonus))
children;
let sep = if spacing then string_space else "" in
(*let rendering = merge_columns sep (List.rev !renderings) in
max_len rendering, rendering *)
merge_columns sep (List.rev !renderings)
let fixed_rendering s =
let s_len = utf8_string_length s in
fun _ -> s_len,[s]
let render_to_strings ~map_unicode_to_tex choose_action size markup =
prerr_endline ("render size is " ^ string_of_int size);
let add_markup attr txt =
let txt = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt in
let value_of_attr (_,_,v) = v in
let title =
try Some (value_of_attr (List.find (fun (_,t,_) -> t = "title") attr))
with _ -> None in
let href =
try Some (value_of_attr (List.find (fun (_,t,_) -> t = "href") attr))
with _ -> None in
match title,href with
| None,None -> txt
| None,Some u -> "" ^ txt ^ ""
| Some t, Some u ->
"" ^ txt ^ ""
| Some t, None ->
let u = "cic:/fakeuri.con" in
"" ^ txt ^ ""
in
let max_size = max_int in
let rec aux_box =
function
| Box.Text (attr, t) ->
fun x ->
(match fixed_rendering t x with
| len, [txt] -> len, [add_markup attr txt]
| _ -> assert false)
| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false
| Box.Action (_, l) -> aux_box (choose_action l)
| Box.Object (_, o) -> fixed_rendering o
| Box.H (attrs, children) ->
let spacing = want_spacing attrs in
let children' = List.map aux_box children in
(fun size -> render_row size spacing children')
| Box.HV (attrs, children) ->
let spacing = want_spacing attrs in
let children' = List.map aux_box children in
(fun size ->
let (size', renderings) as res =
render_row max_size spacing children'
in
if size' <= size then (* children fit in a row *)
res
else (* break needed, re-render using a Box.V *)
aux_box (Box.V (attrs, children)) size)
| Box.V (attrs, []) -> aux_box (Box.Text (attrs,"")) (* FIXME *)
| Box.V (attrs, [child]) -> aux_box child
| Box.V (attrs, hd :: tl) ->
let indent = want_indent attrs in
let hd_f = aux_box hd in
let tl_fs = List.map aux_box tl in
(fun size ->
let hd_rendering = hd_f size in
let children_size =
max 0 (if indent then size - string_indent_len else size)
in
let tl_renderings =
List.map
(fun f ->
(* let indent_header = if indent then string_indent else "" in *)
indent_children (f children_size))
tl_fs
in
List.fold_right
(fun (len,row) (acclen,accrows) -> max acclen len, row@accrows)
(hd_rendering::tl_renderings) (0,[]))
| Box.HOV (attrs, []) -> assert false
| Box.HOV (attrs, [child]) -> aux_box child
| Box.HOV (attrs, children) ->
let spacing = want_spacing attrs in
let indent = want_indent attrs in
let spacing_bonus = if spacing then string_space_len else 0 in
let indent_bonus = if indent then string_indent_len else 0 in
let sep = if spacing then string_space else "" in
let fs = List.map aux_box children in
(fun size ->
let rows = ref [] in
let renderings = ref [] in
let rem_space = ref size in
let first_row = ref true in
let max_len = ref 0 in
let use_rendering (* (space, rendering) *) rendering =
let space, _ = rendering in
let use_indent = !renderings = [] && not !first_row in
let bonus = if use_indent then indent_bonus else spacing_bonus in
let rendering' = (* space+bonus, *)
if use_indent then
space+indent_bonus, List.map indent_string (snd rendering)
else space, (snd rendering)
in
renderings := rendering' :: !renderings;
rem_space := !rem_space - (space + bonus)
in
let end_cluster () =
let new_len, new_rows = merge_columns sep (List.rev !renderings) in
rows := List.rev_append new_rows !rows;
max_len := max !max_len new_len;
rem_space := size - indent_bonus;
renderings := [];
first_row := false
in
List.iter
(fun f ->
let (best_space, _) as best = f max_size in
if best_space <= !rem_space then
use_rendering best
else begin
end_cluster ();
if best_space <= !rem_space then use_rendering best
else use_rendering (f size)
end)
fs;
if !renderings <> [] then end_cluster ();
!max_len, List.rev !rows)
in
snd (aux_box markup size)
let render_to_string ~map_unicode_to_tex choose_action size markup =
String.concat "\n"
(render_to_strings ~map_unicode_to_tex choose_action size markup)