From: Claudio Sacerdoti Coen Date: Tue, 29 Jul 2003 10:55:47 +0000 (+0000) Subject: "(" moved from Mtext to Mo. Spaces removed. X-Git-Tag: LucaOK~20 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11858f45a39c301de590043d3271d95790a52377;p=helm.git "(" moved from Mtext to Mo. Spaces removed. --- diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 575bb687a..65d33f917 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -157,29 +157,34 @@ let make_concl ?(attrs=[]) verb concl = let make_args_for_apply term2pres args = let module Con = Content in let module P = Mpresentation in - let rec make_arg_for_apply is_first arg row = - (match arg with + let make_arg_for_apply is_first arg row = + let res = + match arg with Con.Aux n -> assert false | Con.Premise prem -> let name = (match prem.Con.premise_binder with None -> "previous" | Some s -> s) in - P.smallskip::P.Mi([],name)::row + P.Mi([],name)::row | Con.Lemma lemma -> - P.smallskip::P.Mi([],lemma.Con.lemma_name)::row + P.Mi([],lemma.Con.lemma_name)::row | Con.Term t -> if is_first then (term2pres t)::row - else P.smallskip::P.Mi([],"_")::row + else P.Mi([],"_")::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.smallskip::P.Mi([],"_")::row) in - match args with - hd::tl -> - make_arg_for_apply true hd - (List.fold_right (make_arg_for_apply false) tl []) - | _ -> assert false;; + P.Mi([],"_")::row + in + if is_first then res else P.smallskip::res + in + match args with + hd::tl -> + make_arg_for_apply true hd + (List.fold_right (make_arg_for_apply false) tl []) + | _ -> assert false +;; let rec justification term2pres p = let module Con = Content in @@ -192,7 +197,7 @@ let rec justification term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in P.Mrow([], P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mtext([],"(")::pres_args@[P.Mtext([],")")]) + P.Mo([],"(")::pres_args@[P.Mo([],")")]) else proof2pres term2pres p and proof2pres term2pres p = @@ -290,9 +295,9 @@ and proof2pres term2pres p = P.Mrow ([], [P.Mtext([None,"mathcolor","Red"],"Suppose"); P.Mspace([None,"width","0.1cm"]); - P.Mtext([],"("); + P.Mo([],"("); P.Mi ([],s); - P.Mtext([],")"); + P.Mo([],")"); P.Mspace([None,"width","0.1cm"]); ty]) | None -> @@ -626,9 +631,9 @@ and proof2pres term2pres p = None -> "no name" | Some s -> s) in P.indented (P.Mrow ([], - [P.Mtext([],"("); + [P.Mo([],"("); P.Mi ([],name); - P.Mtext([],")"); + P.Mo([],")"); P.Mspace([None,"width","0.1cm"]); term2pres h.Con.dec_type])) | _ -> assert false in