X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FapplyStylesheets.ml;fp=helm%2FgTopLevel%2FapplyStylesheets.ml;h=3a81e8b86062bc5f1b258cf8ba9fe7faf3ed616d;hb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;hp=0000000000000000000000000000000000000000;hpb=2dc0733271cd251aaa3edaece8a883fe691775ab;p=helm.git diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml new file mode 100644 index 000000000..3a81e8b86 --- /dev/null +++ b/helm/gTopLevel/applyStylesheets.ml @@ -0,0 +1,167 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 30/01/2002 *) +(* *) +(* *) +(******************************************************************************) + +(** stylesheets and parameters list **) + +let parseStyle name = + let style = + Misc.domImpl#createDocumentFromURI + (* ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None *) + ~uri:("styles/" ^ name) () + in + Gdome_xslt.processStylesheet style +;; + +let d_c = parseStyle "drop_coercions.xsl";; +let tc1 = parseStyle "objtheorycontent.xsl";; +let hc2 = parseStyle "content_to_html.xsl";; +let l = parseStyle "link.xsl";; + +let c1 = parseStyle "rootcontent.xsl";; +let g = parseStyle "genmmlid.xsl";; +let c2 = parseStyle "annotatedpres.xsl";; + + +let getterURL = Configuration.getter_url;; +let processorURL = Configuration.processor_url;; + +let mml_styles = [d_c ; c1 ; g ; c2 ; l];; +let mml_args ~explode_all = + ("explodeall",(if explode_all then "true()" else "false()")):: + ["processorURL", "'" ^ processorURL ^ "'" ; + "getterURL", "'" ^ getterURL ^ "'" ; + "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; + "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; + "UNICODEvsSYMBOL", "'symbol'" ; + "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; + "encoding", "'iso-8859-1'" ; + "media-type", "'text/html'" ; + "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; + "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; + "naturalLanguage", "'yes'" ; + "annotations", "'no'" ; + "URLs_or_URIs", "'URIs'" ; + "topurl", "'http://phd.cs.unibo.it/helm'" ; + "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] +;; + +let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; +let sequent_args = + ["processorURL", "'" ^ processorURL ^ "'" ; + "getterURL", "'" ^ getterURL ^ "'" ; + "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; + "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; + "UNICODEvsSYMBOL", "'symbol'" ; + "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; + "encoding", "'iso-8859-1'" ; + "media-type", "'text/html'" ; + "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; + "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; + "naturalLanguage", "'no'" ; + "annotations", "'no'" ; + "explodeall", "true()" ; + "URLs_or_URIs", "'URIs'" ; + "topurl", "'http://phd.cs.unibo.it/helm'" ; + "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 +;; + +let apply_proof_stylesheets proof_doc ~explode_all = + apply_stylesheets proof_doc mml_styles (mml_args ~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 +;;