snapshot

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index bb62f51c98d334818e64eb013b6300e0ca783e3e..8c38cfc0bdaac85941241c1431317fcd4ea0cdde 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -91,8 +91,8 @@ class proof_viewer obj =
       ApplyTransformation.mml_of_cic_object ~explode_all:true
         (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
     in
-    debug_print "load_proof: dumping MathML to /tmp/proof";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ());
+    debug_print "load_proof: dumping MathML to ./proof";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
     match current_mathml with
     |  None ->
         self#load_root ~root:mathml#get_documentElement ;
@@ -165,8 +165,8 @@ class sequent_viewer 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 /tmp/prova";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ());
+    debug_print "load_sequent: dumping MathML to ./prova";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -237,7 +237,6 @@ class sequents_viewer ~(notebook:GPack.notebook)
       sequent_viewer#load_sequent _metasenv goal;
       try
         List.assoc goal goal2win ();
-        debug_print "set_selection none";
         sequent_viewer#set_selection None
       with Not_found -> assert false