X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FapplyStylesheets.ml;fp=helm%2Focaml%2Fcic_transformations%2FapplyStylesheets.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=72f39ea4dc4ce72c93c082d7dd2b49205f6d90c0;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/ocaml/cic_transformations/applyStylesheets.ml b/helm/ocaml/cic_transformations/applyStylesheets.ml deleted file mode 100644 index 72f39ea4d..000000000 --- a/helm/ocaml/cic_transformations/applyStylesheets.ml +++ /dev/null @@ -1,175 +0,0 @@ -(* 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 parseStyles () = - parseStyle "drop_coercions.xsl", - parseStyle "objtheorycontent.xsl", - parseStyle "content_to_html.xsl", - parseStyle "link.xsl", - parseStyle "rootcontent.xsl", - parseStyle "genmmlid.xsl", - parseStyle "annotatedpres.xsl" -;; - -let (d_c,tc1,hc2,l,c1,g,c2) = - let (d_c,tc1,hc2,l,c1,g,c2) = parseStyles () in - ref d_c, ref tc1, ref hc2, ref l, ref c1, ref g, ref c2 -;; - -let reload_stylesheets () = - let (d_c',tc1',hc2',l',c1',g',c2') = parseStyles () in - d_c := d_c'; - tc1 := tc1'; - hc2 := hc2'; - l := l' ; - c1 := c1' ; - g := g' ; - c2 := c2' -;; - - -let mml_styles = [d_c ; c1 ; g ; c2 ; l];; -let mml_args ~explode_all = - ("explodeall",(if explode_all then "true()" else "false()")):: - ["processorURL", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ; - "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ; - "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", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ; - "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ; - "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 () = Helm_registry.get "gtoplevel.inner_types_file";; -let constanttypefile () = Helm_registry.get "gtoplevel.constant_type_file";; - -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 -;; - - - - -