1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
38 Misc.domImpl#createDocumentFromURI
39 (* ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None *)
40 ~uri:("styles/" ^ name) ()
42 Gdome_xslt.processStylesheet style
45 let d_c = parseStyle "drop_coercions.xsl";;
46 let tc1 = parseStyle "objtheorycontent.xsl";;
47 let hc2 = parseStyle "content_to_html.xsl";;
48 let l = parseStyle "link.xsl";;
50 let c1 = parseStyle "rootcontent.xsl";;
51 let g = parseStyle "genmmlid.xsl";;
52 let c2 = parseStyle "annotatedpres.xsl";;
55 let getterURL = Configuration.getter_url;;
56 let processorURL = Configuration.processor_url;;
58 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
59 let mml_args ~explode_all =
60 ("explodeall",(if explode_all then "true()" else "false()"))::
61 ["processorURL", "'" ^ processorURL ^ "'" ;
62 "getterURL", "'" ^ getterURL ^ "'" ;
63 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
64 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
65 "UNICODEvsSYMBOL", "'symbol'" ;
66 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
67 "encoding", "'iso-8859-1'" ;
68 "media-type", "'text/html'" ;
69 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
70 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
71 "naturalLanguage", "'yes'" ;
72 "annotations", "'no'" ;
73 "URLs_or_URIs", "'URIs'" ;
74 "topurl", "'http://phd.cs.unibo.it/helm'" ;
75 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
78 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
80 ["processorURL", "'" ^ processorURL ^ "'" ;
81 "getterURL", "'" ^ getterURL ^ "'" ;
82 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
83 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
84 "UNICODEvsSYMBOL", "'symbol'" ;
85 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
86 "encoding", "'iso-8859-1'" ;
87 "media-type", "'text/html'" ;
88 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
89 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
90 "naturalLanguage", "'no'" ;
91 "annotations", "'no'" ;
92 "explodeall", "true()" ;
93 "URLs_or_URIs", "'URIs'" ;
94 "topurl", "'http://phd.cs.unibo.it/helm'" ;
95 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
98 let apply_stylesheets input styles args =
99 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
103 let apply_proof_stylesheets proof_doc ~explode_all =
104 apply_stylesheets proof_doc mml_styles (mml_args ~explode_all)
107 let apply_sequent_stylesheets sequent_doc =
108 apply_stylesheets sequent_doc sequent_styles sequent_args