(* *)
(***************************************************************************)
+(* $Id$ *)
+
module P = Mpresentation
module B = Box
module Con = Content
match concl with
None -> body
| Some ac ->
- B.Action
- ([None,"type","toggle"],
- [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
- "proof of" ac); body])
+ let concl =
+ make_concl ~attrs:[ Some "helm", "xref", p.Con.proof_id ]
+ "proof of" ac in
+ B.b_toggle [ concl; body ]
in
B.V ([],
[B.Text ([],"(" ^ name ^ ")");
make_row arg proof_conclusion
and andind conclude =
- let proof_conclusion =
- (match conclude.Con.conclude_conclusion with
- None -> B.b_kw "No conclusion???"
- | Some t -> term2pres t) in
let proof,case_arg =
(match conclude.Con.conclude_args with
[Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
| _ -> assert false
and exists conclude =
- let proof_conclusion =
- (match conclude.Con.conclude_conclusion with
- None -> B.b_kw "No conclusion???"
- | Some t -> term2pres t) in
let proof =
(match conclude.Con.conclude_args with
[Con.Aux(n);_;Con.ArgProof proof;_] -> proof
let counter = ref 0
let conjecture2pres term2pres (id, n, context, ty) =
- (B.b_h [Some "helm", "xref", id]
- (((List.map
+ B.b_indent
+ (B.b_hv [Some "helm", "xref", id]
+ ((B.b_toggle [
+ B.b_h [] [B.b_text [] "{...}"; B.b_space];
+ B.b_hv [] (List.map
(function
| None ->
B.b_h []
| Some n -> n)) ;
B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
proof2pres term2pres p])
- (List.rev context)) @
- [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
- B.b_object (p_mi [] (string_of_int n)) ;
- B.b_text [] ":" ;
- term2pres ty ])))
+ (List.rev context)) ] ::
+ [ B.b_h []
+ [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+ B.b_object (p_mi [] (string_of_int n)) ;
+ B.b_text [] ":" ;
+ term2pres ty ]])))
let metasenv2pres term2pres = function
| None -> []