From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Jul 2003 15:46:34 +0000 (+0000)
Subject: - selection attribute of maction is now explicitly generated
X-Git-Tag: LucaOK~41
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b5a5ad620ce04ec43098d7d1f2bcf69eca9743a6;p=helm.git

- selection attribute of maction is now explicitly generated
- all the conjectures are now put in a table to avoid too many
  changes that make Xml Diffing difficult.
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 2404fbea3..9356c2885 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -215,7 +215,8 @@ and proof2pres term2pres p =
                None -> P.Mtext([],"NO PROOF!!!")
              | Some c -> c) in 
           let action = 
-            P.Maction([None,"actiontype","toggle"],
+            P.Maction([None,"actiontype","toggle" ;
+                       None,"selection","1"],
               [(make_concl "proof of" ac);
                 body]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
@@ -620,66 +621,75 @@ let content2pres term2pres (id,params,metasenv,obj) =
          (match metasenv with
              None -> []
            | Some metasenv' ->
-              (P.Mtr []
+              [P.Mtr []
                 [P.Mtd []
-                  (P.Mrow []
-                    [P.Mtext [] "CONJECTURES:"])]) ::
-               List.map
-                (function
-                  (id,n,context,ty) ->
-                    P.Mtr []
-                     [P.Mtd []
-                      (P.Mrow []
-                        (List.map
-                          (function
-                              (_,None) ->
-                                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 []
-                                     (match dec_name with
-                                         None -> "_"
-                                       | Some n -> n) ;
-                                    P.Mo [] ":" ;
-                                    term2pres ty]
-                            | (_,Some (`Definition d)) ->
-                               let
-                                { K.def_name = def_name ;
-                                  K.def_term = bo } = d
-                                in
-                                 P.Mrow []
-                                  [ P.Mi []
-                                     (match def_name with
-                                         None -> "_"
-                                       | Some n -> n) ;
-                                    P.Mo [] ":=" ;
-                                    term2pres bo]
-                            | (_,Some (`Proof p)) ->
-                               let proof_name = p.K.proof_name in
-                                P.Mrow []
-                                 [ P.Mi []
-                                    (match proof_name with
-                                        None -> "_"
-                                      | Some n -> n) ;
-                                   P.Mo [] ":=" ;
-                                   proof2pres term2pres p]
-                          ) context @
-                        [ P.Mo [] "|-" ] @
-                        [ P.Mi [] (string_of_int n) ;
-                          P.Mo [] ":" ;
-                          term2pres ty ]
-                      ))
-                     ]
-                ) metasenv'
-         ) @
+                  (* Conjectures are in their own table to make *)
+                  (* diffing the DOM trees easier.              *)
+                  (P.Mtable
+                    [None,"align","baseline 1";
+                     None,"equalrows","false";
+                     None,"columnalign","left"]
+                   ((P.Mtr []
+                      [P.Mtd []
+                       (P.Mrow []
+                         [P.Mtext [] "CONJECTURES:"])])::
+                    List.map
+                     (function
+                       (id,n,context,ty) ->
+                         P.Mtr []
+                          [P.Mtd []
+                           (P.Mrow []
+                             (List.map
+                               (function
+                                   (_,None) ->
+                                     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 []
+                                          (match dec_name with
+                                              None -> "_"
+                                            | Some n -> n) ;
+                                         P.Mo [] ":" ;
+                                         term2pres ty]
+                                 | (_,Some (`Definition d)) ->
+                                    let
+                                     { K.def_name = def_name ;
+                                       K.def_term = bo } = d
+                                     in
+                                      P.Mrow []
+                                       [ P.Mi []
+                                          (match def_name with
+                                              None -> "_"
+                                            | Some n -> n) ;
+                                         P.Mo [] ":=" ;
+                                         term2pres bo]
+                                 | (_,Some (`Proof p)) ->
+                                    let proof_name = p.K.proof_name in
+                                     P.Mrow []
+                                      [ P.Mi []
+                                         (match proof_name with
+                                             None -> "_"
+                                           | Some n -> n) ;
+                                        P.Mo [] ":=" ;
+                                        proof2pres term2pres p]
+                               ) context @
+                             [ P.Mo [] "|-" ] @
+                             [ P.Mi [] (string_of_int n) ;
+                               P.Mo [] ":" ;
+                               term2pres ty ]
+                           ))
+                          ]
+                     ) metasenv'
+                  ))]]
+         )  @
         [P.Mtr []
           [P.Mtd []
             (P.Mrow []