(* Copyright (C) 2004-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/ *) open Printf module A = NotationPt type markup = string Box.box let to_unicode = Utf8Macro.unicode_of_tex let small_skip = Box.Text ([], " ") let open_paren = Box.Text ([], "(") let closed_paren = Box.Text ([], ")") let semicolon = Box.Text ([], ";") let toggle_action children = Box.Action ([None, "actiontype", "toggle"], children) type child_pos = [ `Left | `Right | `Inner ] let pp_assoc = function | Gramext.LeftA -> "LeftA" | Gramext.RightA -> "RightA" | Gramext.NonA -> "NonA" let rec is_atomic = function | Box.Space _ | Box.Ink _ | Box.Text _ | Box.Object _ -> true | Box.H (_, [box]) | Box.V (_, [box]) | Box.HV (_, [box]) | Box.HOV (_, [box]) | Box.Action (_, [box]) -> is_atomic box | _ -> false let add_parens child_prec curr_prec t = if is_atomic t then ((*prerr_endline ("NOT adding parens around ATOMIC: "^ BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) else if child_prec >= 0 && child_prec < curr_prec then begin (*prerr_endline ("adding parens around: "^ BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*) Box.H ([], [ open_paren; t; closed_paren ]) end else ((*prerr_endline ("NOT adding parens around: "^ BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) let box_of spec attrs children = match children with | [t] -> t | _ -> let kind, spacing, indent = spec in let dress children = if spacing then NotationUtil.dress small_skip children else children in let attrs' = (if spacing then [None, "spacing", "0.5em"] else []) @ (if indent then [None, "indent", "0.5em"] else []) @ attrs in match kind with | A.H -> Box.H (attrs',children) | A.V -> Box.V (attrs',children) | A.HV -> Box.HV (attrs',children) | A.HOV -> Box.HOV (attrs',children) let render status ?(prec=(-1)) = let rec aux prec t = match t with | A.AttributedTerm _ -> aux_attributes [] "" prec t | A.Num (literal, _) -> Box.Text ([], literal) | A.Symbol (literal, Some (None,desc)) -> let literal = to_unicode literal in let attr = [ None, "title", desc ] in Box.Text (attr, literal) | A.Symbol (literal, Some (Some u,desc)) -> let literal = to_unicode literal in let attr = [ None, "title", desc; None, "href", u ] in Box.Text (attr, literal) | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal) | A.Ident (literal, `Uri u) -> let attr = [ None, "href", u ] in let literal = to_unicode literal in Box.Text (attr,literal) | A.Ident (literal, _) -> Box.Text ([], to_unicode literal) | A.Meta(n, l) -> let local_context = Box.Text ([], "["):: (NotationUtil.dress (Box.Text ([], ";")) (List.map (function | None -> Box.Text ([], "_") | Some t -> aux prec t) l)) @ [Box.Text ([], "]")] in Box.H ([], (Box.Text ([], "?"^string_of_int n):: (if (l <> []) then [Box.H ([],local_context)] else []))) | A.Literal (_,`Symbol (s,x)) | A.Literal (_,`Keyword (s,x)) | A.Literal (_,`Number (s,x)) -> let attr = match x with | None, None -> [] | Some u, None -> [ None, "href", u ] | None, Some d -> [ None, "title", d ] | Some u, Some d -> [ None, "href", u; None, "title", d ] in Box.Text (attr, to_unicode s) | A.UserInput -> Box.Text ([], "%") | A.Layout l -> aux_layout prec l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t); assert false and aux_attributes xmlattrs xref prec t = let reset = ref false in let inferred_level = ref None in let expected_level = ref None in let new_xref = ref [] in let new_xmlattrs = ref [] in let rec aux_attribute = function | A.AttributedTerm (attr, t) -> (match attr with | `Loc _ | `Raw _ -> () | `Level (-1) -> reset := true | `Level child_prec -> (* assert (!expected_level = None); *) expected_level := !inferred_level; inferred_level := Some child_prec | `IdRef xref -> new_xref := xref :: !new_xref | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs); aux_attribute t | t -> let prec = match !expected_level with | None -> prec | Some prec -> prec in (match !inferred_level with | None -> aux prec t | Some child_prec -> let t' = aux child_prec t in (*prerr_endline ("inferred: "^string_of_int child_prec^ " exp: "^string_of_int prec ^ " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_->x|_->assert false) 80 t');*) if !reset then ((*prerr_endline "reset";*)t') else add_parens child_prec prec t') in (* prerr_endline (NotationPp.pp_term t); *) aux_attribute t and aux_layout prec l = let attrs = [] in let invoke' t = aux prec t in (* use the one below to reset precedence and associativity *) let invoke_reinit t = aux ~-1 t in match l with | A.Sup (A.Layout (A.Sub (t1,t2)), t3) | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3) -> assert false | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2]) | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2]) | A.Below (t1, t2) -> assert false | A.Above (t1, t2) -> assert false | A.Frac (t1, t2) | A.Over (t1, t2) -> assert false | A.Atop (t1, t2) -> assert false | A.InfRule (t1, t2, t3) -> assert false | A.Sqrt t -> assert false | A.Root (t1, t2) -> assert false | A.Box ((_,spacing,_) as kind, terms) -> let children = aux_children spacing prec (NotationUtil.ungroup terms) in box_of kind attrs children | A.Mstyle (l,terms) -> assert false | A.Mpadded (l,terms) -> assert false | A.Maction alternatives -> toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> assert false | A.Break -> Box.Space [] and aux_children spacing prec terms = let find_clusters = let rec aux_list first clusters acc = function [] when acc = [] -> List.rev clusters | [] -> aux_list first (List.rev acc :: clusters) [] [] | (A.Layout A.Break) :: tl when acc = [] -> aux_list first clusters [] tl | (A.Layout A.Break) :: tl -> aux_list first (List.rev acc :: clusters) [] tl | [hd] -> aux_list false clusters (aux prec hd :: acc) [] | hd :: tl -> aux_list false clusters (aux prec hd :: acc) tl in aux_list true [] [] in let boxify_pres = function [t] -> t | tl -> box_of (A.H, spacing, false) [] tl in List.map boxify_pres (find_clusters terms) in (fun t -> (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*) aux prec t) (* let render_to_boxml id_to_uri t = let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in Xml.add_xml_declaration xml_stream *) let render_context_entry status name = function | A.Decl t -> Box.H ([], [Box.Text([],name); Box.Text([],":"); render status (TermContentPres.pp_ast status t)]) | A.Def (t,ty) -> Box.H ([], [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def"); render status (TermContentPres.pp_ast status t)]) let render_context status context = Box.V ([], Box.Space [None, "width", "0.5em"]:: List.map (fun (name,entry) -> render_context_entry status (to_unicode name) entry) context) let render_sequent status (i,context,ty) = Box.V ([], [render_context status (List.rev context); Box.Ink [None,"width","4cm"; None,"height","2px"]; render status (TermContentPres.pp_ast status ty)])