Minor module re-organization:

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

diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml
index 3eed6f49363c1b19337ed318725e6cf2ff14028c..3a81e8b86062bc5f1b258cf8ba9fe7faf3ed616d 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,57 @@ 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_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
+ 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
+;;