Minor module re-organization:

[helm.git] / helm / gTopLevel / applyStylesheets.ml

diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml
index 61adcb42c17cb4314d942e9c0095b937429e30c6..3a81e8b86062bc5f1b258cf8ba9fe7faf3ed616d 100644 (file)
--- a/helm/gTopLevel/applyStylesheets.ml
+++ b/helm/gTopLevel/applyStylesheets.ml
@@ -130,29 +130,13 @@ let constanttypefile =
   Not_found -> "/public/constanttype"
 ;;
 
-let mml_of_cic_term metano term =
- let metasenv =
-  match !ProofEngine.proof with
-     None -> []
-   | Some (_,metasenv,_,_) -> metasenv
- in
- let context =
-  match !ProofEngine.goal with
-     None -> []
-   | Some metano ->
-      let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> m=metano) metasenv
-      in
-       canonical_context
- in
-   let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
-    SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
-   in
-    let sequent_doc =
-     Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
-    in
-     let res = apply_sequent_stylesheets sequent_doc in
-      res, (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+let mml_of_cic_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 = apply_sequent_stylesheets sequent_doc in
+  sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 ;;
 
 let