]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termViewer.ml
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
[helm.git] / helm / gTopLevel / termViewer.ml
index 913cc95292023719004c229025e7692551b00283..4eac2617a6b4f9cff7949bf4b558715b651b6dc2 100644 (file)
@@ -127,10 +127,10 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
      mml_of_cic_sequent metasenv sequent
    in
+prerr_endline "PRIMA DI SALVARE IL FILE" ;
     self#load_root ~root:sequent_mml#get_documentElement ;
-(*
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
-*)
+prerr_endline "SALVO IL FILE IN TEMP" ;
+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,6 +238,7 @@ 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 () ;
     (match current_mml with
       None ->
         let time1 = Sys.time () in