Major module reorganization:

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

diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml
index 3eed6f49363c1b19337ed318725e6cf2ff14028c..61adcb42c17cb4314d942e9c0095b937429e30c6 100644 (file)
--- a/helm/gTopLevel/applyStylesheets.ml
+++ b/helm/gTopLevel/applyStylesheets.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+(** stylesheets and parameters list **)
+
 let parseStyle name =
  let style =
   Misc.domImpl#createDocumentFromURI
@@ -95,6 +97,8 @@ let sequent_args =
   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 ;;
 
+(** Stylesheets application **)
+
 let apply_stylesheets input styles args =
  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
   input styles
@@ -107,3 +111,73 @@ let apply_proof_stylesheets proof_doc ~explode_all =
 let apply_sequent_stylesheets sequent_doc =
  apply_stylesheets sequent_doc sequent_styles sequent_args
 ;;
+
+(** Utility functions to map objects to MathML Presentation **)
+
+(*CSC: the getter should handle the innertypes, not the FS *)
+
+let innertypesfile =
+ try
+  Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
+ with
+  Not_found -> "/public/innertypes"
+;;
+
+let constanttypefile =
+ try
+  Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
+ with
+  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_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
+=
+(*CSC: ????????????????? *)
+ let xml, bodyxml =
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
+ in
+ let xmlinnertypes =
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
+ in
+  let input =
+   match bodyxml with
+      None -> Xml2Gdome.document_of_xml Misc.domImpl xml
+    | Some bodyxml' ->
+       Xml.pp xml (Some constanttypefile) ;
+       Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
+  in
+(*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
+(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
+(*CSC: local.                                                              *)
+   Xml.pp xmlinnertypes (Some innertypesfile) ;
+   let output = apply_proof_stylesheets input ~explode_all in
+    output
+;;