| Some ac ->
P.Maction
([None,"actiontype","toggle" ; None,"selection","1"],
- [(make_concl "proof of" ac); body])
+ [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
+ "proof of" ac); body])
in
P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
None,"columnalign","left"],
| None ->
prerr_endline "NO NAME!!"; assert false)
| `Proof p ->
- (match p.Con.proof_name with
- Some "w" -> prerr_endline ("processing w");
- | _ -> ());
proof2pres p
| `Definition d ->
(match d.Con.def_name with
let module P = Mpresentation in
let tconclude_body =
match conclude.Con.conclude_conclusion with
- Some t when not omit_conclusion ->
+ Some t when
+ not omit_conclusion or
+ (* CSC: I ignore the omit_conclusion flag in this case. *)
+ (* CSC: Is this the correct behaviour? In the stylesheets *)
+ (* CSC: we simply generated nothing (i.e. the output type *)
+ (* CSC: of the function should become an option. *)
+ conclude.Con.conclude_method = "BU_Conversion" ->
let concl = (term2pres t) in
if conclude.Con.conclude_method = "BU_Conversion" then
make_concl "that is equivalent to" concl
acontext2pres_old p.Con.proof_apply_context true in *)
let body = conclude2pres p.Con.proof_conclude true false in
let presacontext =
+ let acontext_id =
+ match p.Con.proof_apply_context with
+ [] -> p.Con.proof_conclude.Con.conclude_id
+ | {Con.proof_id = id}::_ -> id
+ in
P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
- [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));
+ [P.indented
+ (P.Mtext
+ ([None,"mathcolor","Red" ;
+ Some "helm", "xref", acontext_id],"Proof")) ;
acontext2pres p.Con.proof_apply_context body true]) in
P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
None,"columnalign","left"],
(P.Mrow [Some "helm", "xref", id]
(List.map
(function
- (_,None) ->
+ None ->
P.Mrow []
[ P.Mi [] "_" ;
P.Mo [] ":?" ;
P.Mi [] "_"]
- | (_,Some (`Declaration d))
- | (_,Some (`Hypothesis d)) ->
+ | Some (`Declaration d)
+ | Some (`Hypothesis d) ->
let
{ K.dec_name = dec_name ;
K.dec_type = ty } = d
| Some n -> n) ;
P.Mo [] ":" ;
term2pres ty]
- | (_,Some (`Definition d)) ->
+ | Some (`Definition d) ->
let
{ K.def_name = def_name ;
K.def_term = bo } = d
| Some n -> n) ;
P.Mo [] ":=" ;
term2pres bo]
- | (_,Some (`Proof p)) ->
+ | Some (`Proof p) ->
let proof_name = p.K.proof_name in
P.Mrow []
[ P.Mi []
| Some n -> n) ;
P.Mo [] ":=" ;
proof2pres term2pres p]
- ) context @
+ ) (List.rev context) @
[ P.Mo [] "|-" ] @
[ P.Mi [] (string_of_int n) ;
P.Mo [] ":" ;