X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcontent_pres%2Fcontent2pres.ml;h=abac7cb5deca46fd88f1acf4be241d8ca8b6b5fa;hb=2b2b90087f836c2f32291935216549e9370e68c3;hp=4114d2b5110f7d7855e83c02acab2d49f51a1d9c;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml
index 4114d2b51..abac7cb5d 100644
--- a/helm/ocaml/content_pres/content2pres.ml
+++ b/helm/ocaml/content_pres/content2pres.ml
@@ -32,6 +32,8 @@
 (*                                                                         *)
 (***************************************************************************)
 
+(* $Id$ *)
+
 module P = Mpresentation
 module B = Box
 module Con = Content
@@ -158,10 +160,10 @@ and proof2pres term2pres p =
          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 ^ ")");
@@ -563,10 +565,6 @@ and proof2pres term2pres p =
        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
@@ -619,10 +617,6 @@ and proof2pres term2pres p =
          | _ -> 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
@@ -671,8 +665,11 @@ exception ToDo
 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 []
@@ -713,11 +710,12 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					| 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 -> []