X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=25570868b9385120b76881a667dd1a802d34ea04;hb=21758b512843088d19e81830d9fb121725c8a16e;hp=913cc95292023719004c229025e7692551b00283;hpb=f36273550bc0538ea194cf0dee32ec608a6790f7;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 913cc9529..25570868b 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -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 ; -(* +prerr_endline "SALVO IL FILE IN TEMP" ; 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