ApplyTransformation.mml_of_cic_sequent metasenv sequent
in
current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-(*
- debug_print "load_sequent: dumping MathML to ./prova";
- ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
-*)
+ let name = "sequent_viewer.xml" in
+ prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
+ ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement
end
XmlDiff.update_dom ~from:current_mathml mathml;
mathView#thaw
| _ ->
+ let name = "cic_browser.xml" in
+ prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
+ ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
mathView#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);