]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termViewer.ml
Minor module re-organization:
[helm.git] / helm / gTopLevel / termViewer.ml
index cb3b23a007be0a687bc0fd49e4b9d5f123ca8db1..c35cdb377d700c8df6de42375fa80a34617359ab 100644 (file)
@@ -105,12 +105,8 @@ class sequent_viewer obj =
      ) 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 <-