]> matita.cs.unibo.it Git - helm.git/blob - helm/style/html_init.xsl
New stylesheets from content to html.
[helm.git] / helm / style / html_init.xsl
1 <?xml version="1.0"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
29
30 <!--***********************************************************************--> 
31 <!-- INIT style for HTML                                                   -->
32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
33 <!--***********************************************************************--> 
34
35 <!-- INLINE MODE : BASIC OPERATORS -->
36
37  <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
38        |m:geq|m:gt|m:plus|m:times]">
39   <xsl:variable name="uri">
40    <xsl:value-of select="*[1]/@definitionURL"/>
41   </xsl:variable>
42   <xsl:variable name="symbol">
43    <xsl:choose>
44     <xsl:when test="m:and">
45      <xsl:value-of select="'&#217;'"/>
46     </xsl:when>
47     <xsl:when test="m:or">
48      <xsl:value-of select="'&#218;'"/>
49     </xsl:when>
50     <xsl:when test="m:eq">
51      <xsl:value-of select="'&#61;'"/>
52     </xsl:when>
53     <xsl:when test="m:neq">
54      <xsl:value-of select="'&#185;'"/>
55     </xsl:when>
56     <xsl:when test="m:leq">
57      <xsl:value-of select="'&#163;'"/>
58     </xsl:when>
59     <xsl:when test="m:lt">
60      <xsl:value-of select="'&#60;'"/>
61     </xsl:when>
62     <xsl:when test="m:geq">
63      <xsl:value-of select="'&#179;'"/>
64     </xsl:when>
65     <xsl:when test="m:gt">
66      <xsl:value-of select="'&#62;'"/>
67     </xsl:when>
68     <xsl:when test="m:plus">
69      <xsl:value-of select="'&#43;'"/>
70     </xsl:when>
71     <xsl:when test="m:times">
72      <xsl:value-of select="'&#42;'"/>
73     </xsl:when>
74    </xsl:choose>
75   </xsl:variable>
76   <xsl:text>(</xsl:text>
77   <xsl:apply-templates mode="inline" select="*[2]"/>
78   <a>
79    <xsl:attribute name="href">
80     <xsl:value-of select="concat(string($header),string($uri))"/>
81    </xsl:attribute>
82    <FONT FACE="symbol" mathcolor="blue">
83     <xsl:value-of select="$symbol"/>
84    </FONT>
85   </a>
86   <xsl:apply-templates mode="inline" select="*[3]"/>
87   <xsl:text>)</xsl:text>
88  </xsl:template>
89
90 <!-- INLINE MODE - MINUS (can be unary!) -->
91
92 <xsl:template mode="inline" match="m:apply[m:minus]">
93   <xsl:variable name="uri">
94    <xsl:value-of select="*[1]/@definitionURL"/>
95   </xsl:variable>
96   <xsl:choose>
97    <xsl:when test="count(child::*)=2">
98     <a>
99     <xsl:attribute name="href">
100      <xsl:value-of select="concat(string($header),string($uri))"/>
101     </xsl:attribute>
102     <xsl:text>-</xsl:text>
103     </a>
104     <xsl:apply-templates mode="inline" select="*[2]"/>
105    </xsl:when>
106    <xsl:otherwise>
107     <xsl:text>(</xsl:text>
108     <xsl:apply-templates mode="inline" select="*[2]"/>
109     <a>
110      <xsl:attribute name="href">
111       <xsl:value-of select="concat(string($header),string($uri))"/>
112      </xsl:attribute>
113      <xsl:text>-</xsl:text>
114     </a>
115     <xsl:apply-templates mode="inline" select="*[3]"/>
116     <xsl:text>)</xsl:text>
117    </xsl:otherwise>
118   </xsl:choose>
119  </xsl:template>
120
121 <!-- INLINE MODE NOT -->
122
123  <xsl:template mode="inline" match="m:apply[m:not]">
124   <xsl:variable name="uri">
125    <xsl:value-of select="m:not/@definitionURL"/>
126   </xsl:variable>
127      <a>
128      <xsl:attribute name="href">
129       <xsl:value-of select="concat(string($header),string($uri))"/>
130      </xsl:attribute>
131      <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
132      </a>
133      <xsl:apply-templates mode="inline" select="*[2]"/>
134  </xsl:template>
135
136 <!-- INLINE MODE EXISTS -->
137
138  <xsl:template mode="inline" match="m:apply[m:exists]">
139   <xsl:variable name="uri">
140    <xsl:value-of select="m:exists/@definitionURL"/>
141   </xsl:variable>
142   <a>
143    <xsl:attribute name="href">
144     <xsl:value-of select="concat(string($header),string($uri))"/>
145    </xsl:attribute>
146    <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
147   </a>
148   <xsl:apply-templates select="m:bvar/m:ci"/>
149   <xsl:text>:</xsl:text>
150   <xsl:apply-templates mode="inline" select="m:condition"/>
151   <xsl:text>.</xsl:text>
152   <xsl:apply-templates mode="inline" select="*[last()]"/>
153  </xsl:template>
154
155 <!-- COUNTING MODE -->
156
157 <!-- BASIC OPERATORS -->
158
159  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
160        |m:geq|m:gt|m:plus|m:times]">
161   <xsl:param name="current_indent" select="0"/> 
162   <xsl:param name="width" select="$framewidth"/>
163   <xsl:variable name="uri">
164    <xsl:value-of select="*[1]/@definitionURL"/>
165   </xsl:variable>
166   <xsl:variable name="charlength">
167    <xsl:apply-templates select="*[1]" mode="charcount"/>
168   </xsl:variable>
169   <xsl:variable name="symbol">
170    <xsl:choose>
171     <xsl:when test="m:and">
172      <xsl:value-of select="'&#217;'"/>
173     </xsl:when>
174     <xsl:when test="m:or">
175      <xsl:value-of select="'&#218;'"/>
176     </xsl:when>
177     <xsl:when test="m:eq">
178      <xsl:value-of select="'&#61;'"/>
179     </xsl:when>
180     <xsl:when test="m:neq">
181      <xsl:value-of select="'&#185;'"/>
182     </xsl:when>
183     <xsl:when test="m:leq">
184      <xsl:value-of select="'&#163;'"/>
185     </xsl:when>
186     <xsl:when test="m:lt">
187      <xsl:value-of select="'&#60;'"/>
188     </xsl:when>
189     <xsl:when test="m:geq">
190      <xsl:value-of select="'&#179;'"/>
191     </xsl:when>
192     <xsl:when test="m:gt">
193      <xsl:value-of select="'&#62;'"/>
194     </xsl:when>
195     <xsl:when test="m:plus">
196      <xsl:value-of select="'&#43;'"/>
197     </xsl:when>
198     <xsl:when test="m:times">
199      <xsl:value-of select="'&#42;'"/>
200     </xsl:when>
201    </xsl:choose>
202   </xsl:variable>
203   <xsl:choose>
204     <xsl:when test="$charlength > $framewidth">
205      <xsl:text>(</xsl:text>
206      <xsl:apply-templates select="*[2]">
207       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
208      </xsl:apply-templates>
209      <BR/> 
210      <xsl:call-template name="make_indent">
211       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
212      </xsl:call-template>
213      <a>
214      <xsl:attribute name="href">
215       <xsl:value-of select="concat(string($header),string($uri))"/>
216      </xsl:attribute>
217      <FONT FACE="symbol" mathcolor="blue">
218       <xsl:value-of select="$symbol"/>
219      </FONT>
220      </a>
221      <xsl:apply-templates select="*[3]">
222       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
223      </xsl:apply-templates>
224      <xsl:text>)</xsl:text>
225     </xsl:when>
226     <xsl:otherwise>
227      <xsl:apply-templates mode="inline" select="."/>
228     </xsl:otherwise>
229    </xsl:choose>
230  </xsl:template>
231
232 <!-- MINUS (can be unary!) -->
233
234 <xsl:template match="m:apply[m:minus]">
235   <xsl:param name="current_indent" select="0"/> 
236   <xsl:param name="width" select="$framewidth"/>
237   <xsl:variable name="uri">
238    <xsl:value-of select="*[1]/@definitionURL"/>
239   </xsl:variable>
240   <xsl:choose>
241    <xsl:when test="count(child::*)=2">
242     <a>
243     <xsl:attribute name="href">
244      <xsl:value-of select="concat(string($header),string($uri))"/>
245     </xsl:attribute>
246     <xsl:text>-</xsl:text>
247     </a>
248     <xsl:apply-templates select="*[2]">
249      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
250     </xsl:apply-templates>
251    </xsl:when>
252    <xsl:otherwise>
253     <xsl:variable name="charlength">
254      <xsl:apply-templates select="*[1]" mode="charcount"/>
255     </xsl:variable>
256     <xsl:choose>
257      <xsl:when test="$charlength > $framewidth">
258       <xsl:text>(</xsl:text>
259       <xsl:apply-templates select="*[2]">
260        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
261       </xsl:apply-templates>
262       <BR/> 
263       <xsl:call-template name="make_indent">
264        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
265       </xsl:call-template>
266       <a>
267       <xsl:attribute name="href">
268        <xsl:value-of select="concat(string($header),string($uri))"/>
269       </xsl:attribute>
270       <xsl:text>-</xsl:text>
271       </a>
272       <xsl:apply-templates select="*[3]">
273        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
274       </xsl:apply-templates>
275       <xsl:text>)</xsl:text>
276      </xsl:when>
277      <xsl:otherwise>
278       <xsl:apply-templates mode="inline" select="."/>
279      </xsl:otherwise>
280     </xsl:choose>
281    </xsl:otherwise>
282   </xsl:choose>
283  </xsl:template>
284
285 <!-- NOT -->
286
287  <xsl:template match="m:apply[m:not]">
288   <xsl:param name="current_indent" select="0"/> 
289   <xsl:param name="width" select="$framewidth"/>
290   <xsl:variable name="uri">
291    <xsl:value-of select="m:not/@definitionURL"/>
292   </xsl:variable>
293      <a>
294      <xsl:attribute name="href">
295       <xsl:value-of select="concat(string($header),string($uri))"/>
296      </xsl:attribute>
297      <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
298      </a>
299      <xsl:apply-templates select="*[2]"/>
300  </xsl:template>
301
302 <!-- EXISTS -->
303
304  <xsl:template match="m:apply[m:exists]">
305   <xsl:param name="current_indent" select="0"/> 
306   <xsl:param name="width" select="$framewidth"/>
307   <xsl:variable name="uri">
308    <xsl:value-of select="m:exists/@definitionURL"/>
309   </xsl:variable>
310   <xsl:variable name="charlength">
311    <xsl:apply-templates select="m:exists" mode="charcount"/>
312   </xsl:variable>
313   <xsl:choose>
314     <xsl:when test="$charlength > $framewidth">
315      <a>
316      <xsl:attribute name="href">
317       <xsl:value-of select="concat(string($header),string($uri))"/>
318      </xsl:attribute>
319      <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
320      </a>
321      <xsl:apply-templates select="m:bvar/m:ci"/>
322      <xsl:text>:</xsl:text>
323      <xsl:apply-templates select="m:condition">
324       <xsl:with-param name="current_indent" select="$current_indent + 2 +
325                                 string-length(bvar/ci)"/> 
326      </xsl:apply-templates>
327      <BR/> 
328       <xsl:call-template name="make_indent">
329        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
330       </xsl:call-template>
331      <xsl:text>.</xsl:text>
332       <xsl:apply-templates select="*[last()]">
333        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
334       </xsl:apply-templates>
335     </xsl:when>
336     <xsl:otherwise>
337      <xsl:apply-templates mode="inline" select="."/>
338     </xsl:otherwise>
339    </xsl:choose>
340  </xsl:template>
341
342
343
344
345 <!-- COUNTING -->
346
347 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
348    |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
349 <xsl:param name="incurrent_length" select="0"/> 
350     <xsl:choose>
351     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
352      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
353      <xsl:choose>
354      <xsl:when test="string($siblength) = &quot;&quot;">
355       <xsl:value-of select="$incurrent_length + string-length()"/>
356      </xsl:when>
357      <xsl:otherwise>
358       <xsl:value-of select="number($siblength)"/>
359      </xsl:otherwise>
360      </xsl:choose>
361     </xsl:when>
362     <xsl:otherwise>
363      <xsl:value-of select="$incurrent_length + string-length()"/>
364     </xsl:otherwise>
365     </xsl:choose>
366 </xsl:template> 
367
368 </xsl:stylesheet> 
369
370