From 60c66573ddcb1cea922095dfdc3a315d8d5012a1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 3 Feb 2003 10:50:12 +0000
Subject: [PATCH] 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

---
 helm/gTopLevel/applyStylesheets.ml  | 30 +++++++----------------------
 helm/gTopLevel/applyStylesheets.mli | 16 ++++++---------
 helm/gTopLevel/sequentPp.ml         | 11 +++++------
 helm/gTopLevel/termViewer.ml        |  8 ++------
 4 files changed, 20 insertions(+), 45 deletions(-)

diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml
index 61adcb42c..3a81e8b86 100644
--- 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 ff76c45d5..b450cd992 100644
--- 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 ad8d5bd1d..8cce6e1e3 100644
--- 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 cb3b23a00..c35cdb377 100644
--- 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 <-
-- 
2.39.2