* the transformations have been ported so to generate BoxML + MathML

[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 be363c50b3f66c0e9a4fec787c45f0ef202243e6..ee01f55a99dd527566eac1d868df6769ba7fbede 100644 (file)
--- a/helm/ocaml/cic_transformations/applyTransformation.ml
+++ b/helm/ocaml/cic_transformations/applyTransformation.ml
@@ -43,9 +43,14 @@ 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 = Mpresentation.print_mpres pres_sequent in
-  Xml2Gdome.document_of_xml Misc.domImpl xmlpres,
-    (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+  let xmlpres = Box.document_of_box 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)
+  with
+      e ->
+       prerr_endline ("LUCA: eccezione in document_of_xml " ^ (Printexc.to_string e)) ;
+       raise e
 ;;
 
 let mml_of_cic_object ~explode_all uri acic 
@@ -60,7 +65,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 = Mpresentation.print_mpres pres in
+      let xmlpres = Box.document_of_box pres in
       let time25 = Sys.time () in
       (* alternative: printing to file 
       prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));