From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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