Minor module re-organization:

1. SequentPp is now no more dependent from proofEngine
2. the functions to apply stylesheets from DOM documents to DOM documents
   are not any longer exported by ApplyStylesheets

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

diff --git a/helm/gTopLevel/applyStylesheets.mli b/helm/gTopLevel/applyStylesheets.mli
index ff76c45d5c67af0657179d1050210bd526faab8a..b450cd992db45bd41f678e3655ef4f53caa06404 100644 (file)
--- a/helm/gTopLevel/applyStylesheets.mli
+++ b/helm/gTopLevel/applyStylesheets.mli
@@ -33,17 +33,13 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* Not exported:
-val apply_proof_stylesheets :
- Gdome.document -> explode_all:bool -> Gdome.document
-*)
-val apply_sequent_stylesheets : Gdome.document -> Gdome.document
-
-val mml_of_cic_term :
- int -> Cic.term ->
+val mml_of_cic_sequent :
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
  Gdome.document *
-  (Cic.term * (Cic.id, Cic.term) Hashtbl.t *
-   (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t)
+  ((Cic.id, Cic.term) Hashtbl.t *
+   (Cic.id, Cic.id option) Hashtbl.t *
+   (string, Cic.hypothesis) Hashtbl.t)
 
 val mml_of_cic_object :
   explode_all:bool ->

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index ad8d5bd1d46ffdf0a089c16e6a80277f4e310a95..8cce6e1e39a116e8200bed2a35f2dc339e8841be 100644 (file)
--- a/helm/gTopLevel/sequentPp.ml
+++ b/helm/gTopLevel/sequentPp.ml
@@ -50,12 +50,11 @@ module TextualPp =
   exception NotImplemented;;
 
   let print_sequent (metano,context,goal) =
-   let module P = ProofEngine in
-    "\n" ^
-     let (output,pretty_printer_context_of_context) = print_context context in
-      output ^
-       "---------------------- ?" ^ string_of_int metano ^ "\n" ^
-        CicPp.pp goal pretty_printer_context_of_context
+   "\n" ^
+    let (output,pretty_printer_context_of_context) = print_context context in
+     output ^
+      "---------------------- ?" ^ string_of_int metano ^ "\n" ^
+       CicPp.pp goal pretty_printer_context_of_context
   ;;
  end
 ;;

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index cb3b23a007be0a687bc0fd49e4b9d5f123ca8db1..c35cdb377d700c8df6de42375fa80a34617359ab 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -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 <-