let p_mphantom a b = Mpresentation.Mphantom(a,b)
let b_ink a = Box.Ink a
+module K = Content
+module P = Mpresentation
+
let sequent2pres term2pres (_,_,context,ty) =
- let module K = Content in
- let module P = Mpresentation in
let context2pres context =
let rec aux accum =
function
aux (r::accum) tl
| _::_ -> assert false in
aux [] context in
- let pres_context =
- (Box.b_v
- []
- (context2pres context)) in
+ let pres_context = (Box.b_v [] (context2pres context)) in
let pres_goal = term2pres ty in
- (Box.b_v
- []
- [pres_context;
- b_ink [None,"width","4cm"; None,"height","1px"];
- pres_goal])
-;;
-
-(*
-let sequent2pres ~ids_to_inner_sorts =
- sequent2pres
- (function p ->
- (Cexpr2pres.cexpr2pres_charcount
- (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
-;;
-*)
+ (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 =
-prerr_endline "Sequent2pres.sequent2pres";
sequent2pres
(fun annterm ->
- let (ast, ids_to_uris) as arg =
- Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+ let ast, ids_to_uris =
+ CicNotationRew.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)
+ CicNotationPres.box_of_mpres
+ (CicNotationPres.render ids_to_uris
+ (CicNotationRew.pp_ast ast)))