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
| `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
(* 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)
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