1 (* Copyright (C) 2004-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 type markup = string Box.box
32 let to_unicode = Utf8Macro.unicode_of_tex
34 let small_skip = Box.Text ([], " ")
35 let open_paren = Box.Text ([], "(")
36 let closed_paren = Box.Text ([], ")")
37 let semicolon = Box.Text ([], ";")
39 let toggle_action children =
40 Box.Action ([None, "actiontype", "toggle"], children)
42 type child_pos = [ `Left | `Right | `Inner ]
46 | Gramext.LeftA -> "LeftA"
47 | Gramext.RightA -> "RightA"
48 | Gramext.NonA -> "NonA"
50 let rec is_atomic = function
54 | Box.Object _ -> true
59 | Box.Action (_, [box]) -> is_atomic box
62 let add_parens child_prec curr_prec t =
64 ((*prerr_endline ("NOT adding parens around ATOMIC: "^
65 BoxPp.render_to_string (function x::_->x|_->assert false)
66 ~map_unicode_to_tex:false 80 t);*)t)
67 else if child_prec >= 0 && child_prec < curr_prec then
69 (*prerr_endline ("adding parens around: "^
70 BoxPp.render_to_string (function x::_->x|_->assert false)
71 ~map_unicode_to_tex:false 80 t);*)
72 Box.H ([], [ open_paren; t; closed_paren ])
74 ((*prerr_endline ("NOT adding parens around: "^
75 BoxPp.render_to_string (function x::_->x|_->assert false)
76 ~map_unicode_to_tex:false 80 t);*)t)
78 let box_of spec attrs children =
82 let kind, spacing, indent = spec in
85 NotationUtil.dress small_skip children
90 (if spacing then RenderingAttrs.spacing_attributes `BoxML else [])
91 @ (if indent then RenderingAttrs.indent_attributes `BoxML else [])
95 | A.H -> Box.H (attrs',children)
96 | A.V -> Box.V (attrs',children)
97 | A.HV -> Box.HV (attrs',children)
98 | A.HOV -> Box.HOV (attrs',children)
100 let render status ?(prec=(-1)) =
103 | A.AttributedTerm _ ->
104 aux_attributes [] "" prec t
105 | A.Num (literal, _) -> Box.Text ([], literal)
106 | A.Symbol (literal, _) -> Box.Text ([], literal)
107 | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
111 (NotationUtil.dress (Box.Text ([], ";"))
114 | None -> Box.Text ([], "_")
115 | Some t -> aux prec t) l)) @
119 (Box.Text ([], "?"^string_of_int n)::
120 (if (l <> []) then [Box.H ([],local_context)] else [])))
121 | A.Literal l -> aux_literal prec l
122 | A.UserInput -> Box.Text ([], "%")
123 | A.Layout l -> aux_layout prec l
125 | A.Variable _ -> assert false (* should have been instantiated *)
127 prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
130 and aux_attributes xmlattrs xref prec t =
131 let reset = ref false in
132 let inferred_level = ref None in
133 let expected_level = ref None in
134 let new_xref = ref [] in
135 let new_xmlattrs = ref [] in
136 let rec aux_attribute =
138 | A.AttributedTerm (attr, t) ->
142 | `Level (-1) -> reset := true
143 | `Level child_prec ->
144 (* assert (!expected_level = None); *)
145 expected_level := !inferred_level;
146 inferred_level := Some child_prec
147 | `IdRef xref -> new_xref := xref :: !new_xref
148 | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
152 match !expected_level with
156 (match !inferred_level with
159 let t' = aux child_prec t in
161 ("inferred: "^string_of_int child_prec^
162 " exp: "^string_of_int prec ^
163 " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
164 (function x::_->x|_->assert false) 80 t');*)
166 then ((*prerr_endline "reset";*)t')
167 else add_parens child_prec prec t')
169 (* prerr_endline (NotationPp.pp_term t); *)
172 and aux_literal prec l =
174 | `Symbol s -> Box.Text ([], to_unicode s)
175 | `Keyword s -> Box.Text ([], to_unicode s)
176 | `Number s -> Box.Text ([], to_unicode s))
178 and aux_layout prec l =
180 let invoke' t = aux prec t in
181 (* use the one below to reset precedence and associativity *)
182 let invoke_reinit t = aux ~-1 t in
184 | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
185 | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
187 | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
188 | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
189 | A.Below (t1, t2) -> assert false
190 | A.Above (t1, t2) -> assert false
192 | A.Over (t1, t2) -> assert false
193 | A.Atop (t1, t2) -> assert false
194 | A.InfRule (t1, t2, t3) -> assert false
195 | A.Sqrt t -> assert false
196 | A.Root (t1, t2) -> assert false
197 | A.Box (a, terms) ->
198 let children = List.map (aux prec) terms in
200 | A.Mstyle (l,terms) -> assert false
201 | A.Mpadded (l,terms) -> assert false
202 | A.Maction alternatives ->
203 toggle_action (List.map invoke_reinit alternatives)
204 | A.Group terms -> assert false
205 | A.Break -> Box.Space []
209 (* let render_to_boxml id_to_uri t =
210 let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
211 Xml.add_xml_declaration xml_stream *)
213 let render_context_entry status name = function
216 [Box.Text([],name); Box.Text([],":");
217 render status (TermContentPres.pp_ast status t)])
220 [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def");
221 render status (TermContentPres.pp_ast status t)])
223 let render_context status context =
227 render_context_entry status (to_unicode name) entry) context)
229 let render_sequent status (i,context,ty) =
231 [render_context status context;
232 Box.Ink [None,"width","4cm"; None,"height","2px"];
233 render status (TermContentPres.pp_ast status ty)])