let p_mo a b = Mpresentation.Mo(a,b)
let p_mrow a b = Mpresentation.Mrow(a,b)
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 make_tr r =
- p_mtr [] [p_mtd [] r] in
let context2pres context =
let rec aux accum =
function
K.dec_id = dec_id ;
K.dec_type = ty } = d in
let r =
- p_mrow [Some "helm", "xref", dec_id]
- [ p_mi []
+ Box.b_h [Some "helm", "xref", dec_id]
+ [ Box.b_object (p_mi []
(match dec_name with
None -> "_"
- | Some n -> n) ;
- p_mo [] ":" ;
+ | Some n -> n)) ;
+ Box.b_text [] ":" ;
term2pres ty] in
- aux ((make_tr r)::accum) tl
+ aux (r::accum) tl
| (Some (`Definition d))::tl ->
let
{ K.def_name = def_name ;
K.def_id = def_id ;
K.def_term = bo } = d in
let r =
- p_mrow [Some "helm", "xref", def_id]
- [ p_mi []
+ Box.b_h [Some "helm", "xref", def_id]
+ [ Box.b_object (p_mi []
(match def_name with
None -> "_"
- | Some n -> n) ;
- p_mo [] ":=" ;
+ | Some n -> n)) ;
+ Box.b_text [] ":=" ;
term2pres bo] in
- aux ((make_tr r)::accum) tl
+ aux (r::accum) tl
| _::_ -> assert false in
aux [] context in
- let pres_context =
- make_tr
- (p_mtable
- [None,"align","baseline 1"; None,"equalrows","false";
- None,"columnalign","left"]
- (context2pres context)) in
- let pres_goal =
- make_tr (term2pres ty) in
- (p_mtable
- [None,"align","baseline 1"; None,"equalrows","false";
- None,"columnalign","left"; None,"rowlines","solid"]
- [pres_context;pres_goal])
-;;
+ let pres_context = (Box.b_v [] (context2pres context)) in
+ let pres_goal = term2pres ty in
+ (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)))
-;;
-
-
-
+ sequent2pres
+ (fun annterm ->
+ let ast, ids_to_uris =
+ CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
+ in
+ CicNotationPres.box_of_mpres
+ (CicNotationPres.render ids_to_uris
+ (CicNotationRew.pp_ast ast)))