X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaMathView.ml;h=cd3571ff4322aad73318565bc53e20a1de8003c9;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=f9171068f2158d07ca7dcc1695ed7a638a57d5d6;hpb=789bd6e2f5d8678421c6043359be50b695720d3f;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f9171068f..cd3571ff4 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -167,10 +167,9 @@ class sequentViewer obj =
       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
 
@@ -556,6 +555,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           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);