aux_mpres t
let add_parens child_prec curr_prec t =
-(* eprintf
- ("add_parens: " ^^
- "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!")
- child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
- curr_prec; *)
- if is_atomic t then t
-(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *)
- else if child_prec >= 0 && child_prec <= curr_prec then
- begin (* parens should be added *)
-(* prerr_endline "adding parens!"; *)
+ 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);*)
match t with
| Mpresentation.Mobject (_, box) ->
mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
| mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
end else
- t
+ ((*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 ids_to_uris ?(prec=(-1)) =
+let lookup_uri ids_to_uris id =
+ try
+ let uri = Hashtbl.find ids_to_uris id in
+ Some (UriManager.string_of_uri uri)
+ with Not_found -> None
+;;
+
+let render ~lookup_uri ?(prec=(-1)) =
let module A = Ast in
let module P = Mpresentation in
(* let use_unicode = true in *)
- let lookup_uri id =
- (try
- let uri = Hashtbl.find ids_to_uris id in
- Some (UriManager.string_of_uri uri)
- with Not_found -> None)
- in
let make_href xmlattrs xref =
let xref_uris =
List.fold_right
let expected_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
-(* let reinit = ref false in *)
let rec aux_attribute =
function
| A.AttributedTerm (attr, t) ->
| `Raw _ -> ()
| `Level (-1) -> reset := true
| `Level child_prec ->
- assert (!expected_level = None);
+(* assert (!expected_level = None); *)
expected_level := !inferred_level;
inferred_level := Some child_prec
| `IdRef xref -> new_xref := xref :: !new_xref
| Some prec -> prec
in
(match !inferred_level with
- | None -> aux !new_xmlattrs mathonly new_xref prec t
+ | None -> aux !new_xmlattrs mathonly new_xref prec t
| Some child_prec ->
- let t' =
- aux !new_xmlattrs mathonly new_xref child_prec t in
+ let t' = aux !new_xmlattrs mathonly new_xref 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 t'
+ then ((*prerr_endline "reset";*)t')
else add_parens child_prec prec t')
in
+(* prerr_endline (CicNotationPp.pp_term t); *)
aux_attribute t
and aux_literal xmlattrs xref prec l =
let attrs = make_href xmlattrs xref in
(* use the one below to reset precedence and associativity *)
let invoke_reinit t = aux [] mathonly xref ~-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)
+ -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3)
| A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
| A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
| A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2)
| A.Atop (t1, t2) ->
Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1,
invoke_reinit t2)
+ | A.InfRule (t1, t2, t3) ->
+ Mpres.Mstyle ([None,"mathsize","big"],
+ Mpres.Mrow (attrs,
+ [Mpres.Mfrac ([],
+ Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1),
+ Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2));
+ Mpres.Mstyle ([None,"scriptlevel","2"],
+ Mpresentation.Mspace
+ (RenderingAttrs.small_skip_attributes `MathML));
+ Mpres.Mstyle ([None,"scriptlevel","1"],invoke_reinit t3)]))
| A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t)
| A.Root (t1, t2) ->
Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)
(CicNotationUtil.ungroup terms)
in
box_of mathonly kind attrs children
+ | A.Mstyle (l,terms) ->
+ Mpres.Mstyle
+ (List.map (fun (k,v) -> None,k,v) l,
+ box_of mathonly (A.H, false, false) attrs
+ (aux_children mathonly false xref prec
+ (CicNotationUtil.ungroup terms)))
+ | A.Mpadded (l,terms) ->
+ Mpres.Mpadded
+ (List.map (fun (k,v) -> None,k,v) l,
+ box_of mathonly (A.H, false, false) attrs
+ (aux_children mathonly false xref prec
+ (CicNotationUtil.ungroup terms)))
+ | A.Maction alternatives ->
+ toggle_action (List.map invoke_reinit alternatives)
| A.Group terms ->
let children =
aux_children mathonly false xref prec
projects / helm.git / blobdiff