[]
(context2pres context)) in
let pres_goal = term2pres ty in
- (Box.b_v
- []
- [pres_context;
- b_ink [None,"width","4cm"; None,"height","1px"];
- pres_goal])
+ (Box.b_h [] [
+ Box.b_space;
+ (Box.b_v []
+ [Box.b_space;
+ pres_context;
+ b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+ Box.b_space;
+ pres_goal])
+ ])
;;
+(*
let sequent2pres ~ids_to_inner_sorts =
sequent2pres
(function p ->
(Cexpr2pres.cexpr2pres_charcount
(Content_expressions.acic2cexpr ids_to_inner_sorts p)))
;;
+*)
-
-
+let sequent2pres ~ids_to_inner_sorts =
+ sequent2pres
+ (fun annterm ->
+ let (ast, ids_to_uris) as arg =
+ Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+ in
+ let astbox = Ast2pres.ast2astBox arg in
+ Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astbox)