X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=b7de8499a1404df236de4459ae606626ad73f7e2;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=57d7d9140a9868d147147cd49774b0ce710732c2;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 57d7d9140..b7de8499a 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -42,9 +42,10 @@ 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
 
+module K = Content
+module P = Mpresentation
+
 let sequent2pres term2pres (_,_,context,ty) =
- let module K = Content in
- let module P = Mpresentation in
    let context2pres context = 
      let rec aux accum =
      function 
@@ -75,39 +76,29 @@ let sequent2pres term2pres (_,_,context,ty) =
                 (match def_name with
                    None -> "_"
                  | Some n -> n)) ;
-                 Box.b_text [] ":=" ;
+                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
                 term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
- let pres_context = 
-    (Box.b_v
-      []
-      (context2pres context)) in
+ let pres_context = (Box.b_v [] (context2pres context)) in
  let pres_goal = term2pres ty in 
- (Box.b_v
-    []
-    [pres_context;
-     b_ink [None,"width","4cm"; None,"height","1px"];
-     pres_goal])
-;;
-
-(*
-let sequent2pres ~ids_to_inner_sorts =
- sequent2pres 
-  (function p -> 
-   (Cexpr2pres.cexpr2pres_charcount 
-    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
-;;
-*)
+ (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 =
-prerr_endline "Sequent2pres.sequent2pres";
   sequent2pres
     (fun annterm ->
-      let (ast, ids_to_uris) as arg =
-        Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+      let ast, ids_to_uris =
+        CicNotationRew.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)
+      CicNotationPres.box_of_mpres
+        (CicNotationPres.render ids_to_uris
+          (CicNotationRew.pp_ast ast)))