X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FapplyTransformation.ml;h=e1b36ea5c379697fbb191a85f1966622cb3f2d74;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=c70f46c68bb3e034034a5b4f664e5cd92808bab5;hpb=cfaa4ba59014ccb6046a2a672e97a5e88d7d2946;p=helm.git

diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml
index c70f46c68..e1b36ea5c 100644
--- 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,9 +47,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 = 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)
+  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 +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 = Mpresentation.print_mpres 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)));
@@ -75,3 +84,9 @@ let mml_of_cic_object ~explode_all uri acic
    | _ -> assert false
 ;;
 
+(*
+let _ =
+ Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
+;;
+*)
+