X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=ad2724134f47562b6c0c58633a3941a26b7a8967;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=4c47bc51aa47fe28320627d88706614e52b729f0;hpb=cfaa4ba59014ccb6046a2a672e97a5e88d7d2946;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 4c47bc51a..ad2724134 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -40,12 +40,11 @@ let p_mi a b = Mpresentation.Mi(a,b)
 let p_mo a b = Mpresentation.Mo(a,b)
 let p_mrow a b = Mpresentation.Mrow(a,b)
 let p_mphantom a b = Mpresentation.Mphantom(a,b)
+let b_ink a = Box.Ink a
 
 let sequent2pres term2pres (_,_,context,ty) =
  let module K = Content in
  let module P = Mpresentation in
-   let make_tr r =
-      p_mtr [] [p_mtd [] r] in
    let context2pres context = 
      let rec aux accum =
      function 
@@ -57,51 +56,61 @@ let sequent2pres term2pres (_,_,context,ty) =
              K.dec_id = dec_id ;
              K.dec_type = ty } = d in
          let r = 
-           p_mrow [Some "helm", "xref", dec_id] 
-             [ p_mi []
+           Box.b_h [Some "helm", "xref", dec_id] 
+             [ Box.b_object (p_mi []
                (match dec_name with
                   None -> "_"
-                | Some n -> n) ;
-               p_mo [] ":" ;
+                | Some n -> n)) ;
+               Box.b_text [] ":" ;
                term2pres ty] in
-         aux ((make_tr r)::accum) tl
+         aux (r::accum) tl
      | (Some (`Definition d))::tl ->
          let
            { K.def_name = def_name ;
              K.def_id = def_id ;
              K.def_term = bo } = d in
          let r = 
-            p_mrow [Some "helm", "xref", def_id]
-              [ p_mi []
+            Box.b_h [Some "helm", "xref", def_id]
+              [ Box.b_object (p_mi []
                 (match def_name with
                    None -> "_"
-                 | Some n -> n) ;
-                 p_mo [] ":=" ;
+                 | Some n -> n)) ;
+                 Box.b_text [] ":=" ;
                 term2pres bo] in
-         aux ((make_tr r)::accum) tl
+         aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
  let pres_context = 
-   make_tr 
-    (p_mtable
-      [None,"align","baseline 1"; None,"equalrows","false"; 
-       None,"columnalign","left"]
+    (Box.b_v
+      []
       (context2pres context)) in
- let pres_goal = 
-   make_tr (term2pres ty) in 
- (p_mtable
-   [None,"align","baseline 1"; None,"equalrows","false"; 
-    None,"columnalign","left"; None,"rowlines","solid"] 
-    [pres_context;pres_goal])
+ let pres_goal = term2pres ty in 
+ (Box.b_h [] [
+   Box.b_space; 
+   (Box.b_v []
+      [Box.b_space;
+       pres_context;
+       b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+       Box.b_space; 
+       pres_goal])
+ ])
 ;;
 
+(*
 let sequent2pres ~ids_to_inner_sorts =
  sequent2pres 
   (function p -> 
    (Cexpr2pres.cexpr2pres_charcount 
     (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
 ;;
+*)
 
-
-
+let sequent2pres ~ids_to_inner_sorts =
+  sequent2pres
+    (fun annterm ->
+      let (ast, ids_to_uris) as arg =
+        Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+      in
+      let astbox = Ast2pres.ast2astBox arg in
+      Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astbox)