+let refresh_proof (output : GMathView.math_view) =
+ let currentproof =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty)
+ in
+ let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) =
+ Cic2acic.acic_object_of_cic_object currentproof
+ in
+ let mml = mml_of_cic_object acic ids_to_inner_sorts in
+ output#load_tree mml ;
+ current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+;;
+
+let refresh_sequent (proofw : GMathView.math_view) =
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let currentsequent =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some (_,sequent) -> sequent
+ in
+ let sequent_gdome = SequentPp.XmlPp.print_sequent metasenv currentsequent in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ proofw#load_tree ~dom:sequent_mml
+(*
+ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
+ ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
+ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
+ ~name:"/public/sacerdot/guruguru2" ~indent:true ())
+*)
+;;
+