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 =
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
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)));
| _ -> assert false
;;
+(*
let _ =
Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
;;
+*)