]> matita.cs.unibo.it Git - helm.git/blob - helm/style/html_init.xsl
characters in symbol font unified in size
[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 href="{$uri}">
79    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
80     <xsl:value-of select="$symbol"/>
81    </FONT>
82   </a>
83   <xsl:apply-templates mode="inline" select="*[3]"/>
84   <xsl:text>)</xsl:text>
85  </xsl:template>
86
87 <!-- INLINE MODE - MINUS (can be unary!) -->
88
89 <xsl:template mode="inline" match="m:apply[m:minus]">
90   <xsl:variable name="uri">
91    <xsl:value-of select="*[1]/@definitionURL"/>
92   </xsl:variable>
93   <xsl:choose>
94    <xsl:when test="count(child::*)=2">
95     <a href="{$uri}">
96     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
97     </a>
98     <xsl:apply-templates mode="inline" select="*[2]"/>
99    </xsl:when>
100    <xsl:otherwise>
101     <xsl:text>(</xsl:text>
102     <xsl:apply-templates mode="inline" select="*[2]"/>
103     <a href="{$uri}">
104      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
105     </a>
106     <xsl:apply-templates mode="inline" select="*[3]"/>
107     <xsl:text>)</xsl:text>
108    </xsl:otherwise>
109   </xsl:choose>
110  </xsl:template>
111
112 <!-- INLINE MODE NOT -->
113
114  <xsl:template mode="inline" match="m:apply[m:not]">
115   <xsl:variable name="uri">
116    <xsl:value-of select="m:not/@definitionURL"/>
117   </xsl:variable>
118      <a href="{$uri}">
119      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#216;</FONT>
120      </a>
121      <xsl:apply-templates mode="inline" select="*[2]"/>
122  </xsl:template>
123
124 <!-- INLINE MODE EXISTS -->
125
126  <xsl:template mode="inline" match="m:apply[m:exists]">
127   <xsl:variable name="uri">
128    <xsl:value-of select="m:exists/@definitionURL"/>
129   </xsl:variable>
130   <a href="{$uri}">
131    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#36;</FONT>
132   </a>
133   <xsl:apply-templates select="m:bvar/m:ci"/>
134   <xsl:text>:</xsl:text>
135   <xsl:apply-templates mode="inline" select="m:condition"/>
136   <xsl:text>.</xsl:text>
137   <xsl:apply-templates mode="inline" select="*[last()]"/>
138  </xsl:template>
139
140 <!-- COUNTING MODE -->
141
142 <!-- BASIC OPERATORS -->
143
144  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
145        |m:geq|m:gt|m:plus|m:times]">
146   <xsl:param name="current_indent" select="0"/> 
147   <xsl:param name="width" select="$framewidth"/>
148   <xsl:variable name="uri">
149    <xsl:value-of select="*[1]/@definitionURL"/>
150   </xsl:variable>
151   <xsl:variable name="charlength">
152    <xsl:apply-templates select="*[1]" mode="charcount"/>
153   </xsl:variable>
154   <xsl:variable name="symbol">
155    <xsl:choose>
156     <xsl:when test="m:and">
157      <xsl:value-of select="'&#217;'"/>
158     </xsl:when>
159     <xsl:when test="m:or">
160      <xsl:value-of select="'&#218;'"/>
161     </xsl:when>
162     <xsl:when test="m:eq">
163      <xsl:value-of select="'&#61;'"/>
164     </xsl:when>
165     <xsl:when test="m:neq">
166      <xsl:value-of select="'&#185;'"/>
167     </xsl:when>
168     <xsl:when test="m:leq">
169      <xsl:value-of select="'&#163;'"/>
170     </xsl:when>
171     <xsl:when test="m:lt">
172      <xsl:value-of select="'&#60;'"/>
173     </xsl:when>
174     <xsl:when test="m:geq">
175      <xsl:value-of select="'&#179;'"/>
176     </xsl:when>
177     <xsl:when test="m:gt">
178      <xsl:value-of select="'&#62;'"/>
179     </xsl:when>
180     <xsl:when test="m:plus">
181      <xsl:value-of select="'&#43;'"/>
182     </xsl:when>
183     <xsl:when test="m:times">
184      <xsl:value-of select="'&#42;'"/>
185     </xsl:when>
186    </xsl:choose>
187   </xsl:variable>
188   <xsl:choose>
189     <xsl:when test="$charlength > $framewidth">
190      <xsl:text>(</xsl:text>
191      <xsl:apply-templates select="*[2]">
192       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
193      </xsl:apply-templates>
194      <BR/> 
195      <xsl:call-template name="make_indent">
196       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
197      </xsl:call-template>
198      <a href="{$uri}">
199      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
200       <xsl:value-of select="$symbol"/>
201      </FONT>
202      </a>
203      <xsl:apply-templates select="*[3]">
204       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
205      </xsl:apply-templates>
206      <xsl:text>)</xsl:text>
207     </xsl:when>
208     <xsl:otherwise>
209      <xsl:apply-templates mode="inline" select="."/>
210     </xsl:otherwise>
211    </xsl:choose>
212  </xsl:template>
213
214 <!-- MINUS (can be unary!) -->
215
216 <xsl:template match="m:apply[m:minus]">
217   <xsl:param name="current_indent" select="0"/> 
218   <xsl:param name="width" select="$framewidth"/>
219   <xsl:variable name="uri">
220    <xsl:value-of select="*[1]/@definitionURL"/>
221   </xsl:variable>
222   <xsl:choose>
223    <xsl:when test="count(child::*)=2">
224     <a href="{$uri}">
225     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
226     </a>
227     <xsl:apply-templates select="*[2]">
228      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
229     </xsl:apply-templates>
230    </xsl:when>
231    <xsl:otherwise>
232     <xsl:variable name="charlength">
233      <xsl:apply-templates select="*[1]" mode="charcount"/>
234     </xsl:variable>
235     <xsl:choose>
236      <xsl:when test="$charlength > $framewidth">
237       <xsl:text>(</xsl:text>
238       <xsl:apply-templates select="*[2]">
239        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
240       </xsl:apply-templates>
241       <BR/> 
242       <xsl:call-template name="make_indent">
243        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
244       </xsl:call-template>
245       <a href="{$uri}">
246       <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
247       </a>
248       <xsl:apply-templates select="*[3]">
249        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
250       </xsl:apply-templates>
251       <xsl:text>)</xsl:text>
252      </xsl:when>
253      <xsl:otherwise>
254       <xsl:apply-templates mode="inline" select="."/>
255      </xsl:otherwise>
256     </xsl:choose>
257    </xsl:otherwise>
258   </xsl:choose>
259  </xsl:template>
260
261 <!-- NOT -->
262
263  <xsl:template match="m:apply[m:not]">
264   <xsl:param name="current_indent" select="0"/> 
265   <xsl:param name="width" select="$framewidth"/>
266   <xsl:variable name="uri">
267    <xsl:value-of select="m:not/@definitionURL"/>
268   </xsl:variable>
269      <a href="{$uri}">
270      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#216;</FONT>
271      </a>
272      <xsl:apply-templates select="*[2]"/>
273  </xsl:template>
274
275 <!-- EXISTS -->
276
277  <xsl:template match="m:apply[m:exists]">
278   <xsl:param name="current_indent" select="0"/> 
279   <xsl:param name="width" select="$framewidth"/>
280   <xsl:variable name="uri">
281    <xsl:value-of select="m:exists/@definitionURL"/>
282   </xsl:variable>
283   <xsl:variable name="charlength">
284    <xsl:apply-templates select="m:exists" mode="charcount"/>
285   </xsl:variable>
286   <xsl:choose>
287     <xsl:when test="$charlength > $framewidth">
288      <a href="{$uri}">
289       <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#36;</FONT>
290      </a>
291      <xsl:apply-templates select="m:bvar/m:ci"/>
292      <xsl:text>:</xsl:text>
293      <xsl:apply-templates select="m:condition">
294       <xsl:with-param name="current_indent" select="$current_indent + 2 +
295                                 string-length(bvar/ci)"/> 
296      </xsl:apply-templates>
297      <BR/> 
298       <xsl:call-template name="make_indent">
299        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
300       </xsl:call-template>
301      <xsl:text>.</xsl:text>
302       <xsl:apply-templates select="*[last()]">
303        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
304       </xsl:apply-templates>
305     </xsl:when>
306     <xsl:otherwise>
307      <xsl:apply-templates mode="inline" select="."/>
308     </xsl:otherwise>
309    </xsl:choose>
310  </xsl:template>
311
312
313
314
315 <!-- COUNTING -->
316
317 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
318    |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
319 <xsl:param name="incurrent_length" select="0"/> 
320     <xsl:choose>
321     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
322      <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>
323      <xsl:choose>
324      <xsl:when test="string($siblength) = &quot;&quot;">
325       <xsl:value-of select="$incurrent_length + string-length()"/>
326      </xsl:when>
327      <xsl:otherwise>
328       <xsl:value-of select="number($siblength)"/>
329      </xsl:otherwise>
330      </xsl:choose>
331     </xsl:when>
332     <xsl:otherwise>
333      <xsl:value-of select="$incurrent_length + string-length()"/>
334     </xsl:otherwise>
335     </xsl:choose>
336 </xsl:template> 
337
338 </xsl:stylesheet> 
339
340