) selections
method load_sequent metasenv sequent =
- let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
- SequentPp.XmlPp.print_sequent metasenv sequent in
- let sequent_doc =
- Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
- let sequent_mml =
- ApplyStylesheets.apply_sequent_stylesheets sequent_doc
+ let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+ ApplyStylesheets.mml_of_cic_sequent metasenv sequent
in
self#load_doc ~dom:sequent_mml ;
current_infos <-