let open_paren = Mpresentation.Mo ([], "(")
let closed_paren = Mpresentation.Mo ([], ")")
+let open_bracket = Mpresentation.Mo ([], "[")
+let closed_bracket = Mpresentation.Mo ([], "]")
let open_brace = Mpresentation.Mo ([], "{")
let closed_brace = Mpresentation.Mo ([], "}")
let hidden_substs = Mpresentation.Mtext ([], "{...}")
+let hidden_lctxt = Mpresentation.Mtext ([], "[...]")
let open_box_paren = Box.Text ([], "(")
let closed_box_paren = Box.Text ([], ")")
let semicolon = Mpresentation.Mo ([], ";")
end else
t
-let render ids_to_uris =
+let render ids_to_uris ?(prec=(-1)) =
let module A = Ast in
let module P = Mpresentation in
(* let use_unicode = true in *)
in
let substs_maction = toggle_action [ hidden_substs; substs' ] in
box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+ | A.Meta(n, l) ->
+ let local_context l =
+ box_of mathonly (A.H, false, false) []
+ ([ Mpres.Mtext ([], "[") ] @
+ (CicNotationUtil.dress (Mpres.Mtext ([], ";"))
+ (List.map
+ (function
+ | None -> Mpres.Mtext ([], "_")
+ | Some t -> aux xmlattrs mathonly xref pos prec t) l)) @
+ [ Mpres.Mtext ([], "]")])
+ in
+ let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in
+ box_of mathonly (A.H, false, false) []
+ ([Mpres.Mtext ([], "?"^string_of_int n) ]
+ @ (if l <> [] then [lctxt_maction] else []))
| A.Literal l -> aux_literal xmlattrs xref prec l
| A.UserInput -> Mpres.Mtext ([], "%")
| A.Layout l -> aux_layout mathonly xref pos prec l
in
List.map boxify_pres (find_clusters terms)
in
- aux [] false (ref []) `Inner ~-1
+ aux [] false (ref []) `Inner prec
let rec print_box (t: boxml_markup) =
Box.box2xml print_mpres t