(* 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 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 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, _) -> Box.Text ([], 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 l -> aux_literal prec l | 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_literal prec l = (match l with | `Symbol s -> Box.Text ([], to_unicode s) | `Keyword s -> Box.Text ([], to_unicode s) | `Number s -> Box.Text ([], to_unicode s)) 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 (a, terms) -> let children = List.map (aux prec) terms in Box.H([],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 [] in aux prec (* 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 ([], 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 context; Box.Ink [None,"width","4cm"; None,"height","2px"]; render status (TermContentPres.pp_ast status ty)])