transformations no longer use Content_expression, but rather CicAst

[helm.git] / helm / ocaml / cic_transformations / applyTransformation.ml

diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml
index ee01f55a99dd527566eac1d868df6769ba7fbede..e1b36ea5c379697fbb191a85f1966622cb3f2d74 100644 (file)
--- a/helm/ocaml/cic_transformations/applyTransformation.ml
+++ b/helm/ocaml/cic_transformations/applyTransformation.ml
@@ -36,6 +36,10 @@
 let reload_stylesheets = ignore
 ;;
 
+let mpres_document pres_box =
+  Ast2pres.add_xml_declaration
+    (Box.box2xml ~obj2xml:Mpresentation.print_mpres pres_box)
+
 let mml_of_cic_sequent metasenv sequent =
   let asequent,ids_to_terms,
     ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses =
@@ -43,7 +47,7 @@ let mml_of_cic_sequent metasenv sequent =
   let content_sequent = Cic2content.map_sequent asequent in 
   let pres_sequent = 
     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
-  let xmlpres = Box.document_of_box pres_sequent in
+  let xmlpres = mpres_document pres_sequent in
   (*  Xml.pp_to_outchan xmlpres stdout ; *)
   try
     Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
@@ -65,7 +69,7 @@ let mml_of_cic_object ~explode_all uri acic
       let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
       let time2 = Sys.time () in
       (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
-      let xmlpres = Box.document_of_box pres in
+      let xmlpres = mpres_document pres in
       let time25 = Sys.time () in
       (* alternative: printing to file 
       prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
@@ -80,7 +84,9 @@ let mml_of_cic_object ~explode_all uri acic
    | _ -> assert false
 ;;
 
+(*
 let _ =
  Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
 ;;
+*)