ported to new xpointer syntax

[helm.git] / helm / gTopLevel / termViewer.ml

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index bd7d0066dc9bcced6082d94612d7a526b61af296..b6ca2a532922e3cb42b1b4f7796d51a78dcfa8bb 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -130,7 +130,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
 prerr_endline "PRIMA DI SALVARE IL FILE" ;
     self#load_root ~root:sequent_mml#get_documentElement ;
 prerr_endline "SALVO IL FILE IN TEMP" ;
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
+ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
@@ -238,13 +238,12 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
     (* self#load_doc ~dom:mml ;
        current_mml <- Some mml ; *)
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
+    ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
     (match current_mml with
       None ->
         let time1 = Sys.time () in
         self#load_root ~root:mml#get_documentElement ;
         let time2 = Sys.time () in
-       prerr_endline "LUCA: PASSO DA DOVE DEVO PASSARE" ; 
         debug_print ("Loading and displaying the proof took " ^
           string_of_float (time2 -. time1) ^ "seconds") ;
         current_mml <- Some mml