(* *)
(***************************************************************************)
+let p_mtr a b = Mpresentation.Mtr(a,b)
+let p_mtd a b = Mpresentation.Mtd(a,b)
+let p_mtable a b = Mpresentation.Mtable(a,b)
+let p_mtext a b = Mpresentation.Mtext(a,b)
+let p_mi a b = Mpresentation.Mi(a,b)
+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 rec split n l =
if n = 0 then [],l
else let l1,l2 =
| _ -> assert false) in
(match conclude.Con.conclude_conclusion with
None ->
- P.Mrow []
- [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+ p_mrow []
+ [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
| Some c -> let conclusion = term2pres c in
make_row
[arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
let module P = Mpresentation in
match obj with
`Def (K.Const,thesis,`Proof p) ->
- P.Mtable
+ p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left";
None,"helm:xref","id"]
- ([P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext []
+ ([p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext []
("UNFINISHED PROOF" ^ id ^"(" ^
String.concat " ; " (List.map UriManager.string_of_uri params)^
")")])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "THESIS:"])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mphantom []
- (P.Mtext [] "__") ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "THESIS:"])] ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mphantom []
+ (p_mtext [] "__") ;
term2pres thesis])]] @
(match metasenv with
None -> []
| Some metasenv' ->
- [P.Mtr []
- [P.Mtd []
+ [p_mtr []
+ [p_mtd []
(* Conjectures are in their own table to make *)
(* diffing the DOM trees easier. *)
- (P.Mtable
+ (p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left"]
- ((P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "CONJECTURES:"])])::
+ ((p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "CONJECTURES:"])])::
List.map
(function
(id,n,context,ty) ->
- P.Mtr []
- [P.Mtd []
- (P.Mrow [Some "helm", "xref", id]
+ p_mtr []
+ [p_mtd []
+ (p_mrow [Some "helm", "xref", id]
(List.map
(function
None ->
- P.Mrow []
- [ P.Mi [] "_" ;
- P.Mo [] ":?" ;
- P.Mi [] "_"]
+ p_mrow []
+ [ p_mi [] "_" ;
+ p_mo [] ":?" ;
+ p_mi [] "_"]
| Some (`Declaration d)
| Some (`Hypothesis d) ->
let
{ K.dec_name = dec_name ;
K.dec_type = ty } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match dec_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":" ;
+ p_mo [] ":" ;
term2pres ty]
| Some (`Definition d) ->
let
{ K.def_name = def_name ;
K.def_term = bo } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match def_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
term2pres bo]
| Some (`Proof p) ->
let proof_name = p.K.proof_name in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match proof_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
proof2pres term2pres p]
) (List.rev context) @
- [ P.Mo [] "|-" ] @
- [ P.Mi [] (string_of_int n) ;
- P.Mo [] ":" ;
+ [ p_mo [] "|-" ] @
+ [ p_mi [] (string_of_int n) ;
+ p_mo [] ":" ;
term2pres ty ]
))
]
) metasenv'
))]]
) @
- [P.Mtr []
- [P.Mtd []
- (P.Mrow []
+ [p_mtr []
+ [p_mtd []
+ (p_mrow []
[proof2pres term2pres p])]])
| _ -> raise ToDo
;;