]> matita.cs.unibo.it Git - helm.git/blob - helm/style/html_reals.xsl
Initial revision
[helm.git] / helm / style / html_reals.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 <xsl:template name="mksymbol-reals">
36  <xsl:param name="symbol" select="''"/>
37   <xsl:choose>
38    <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
39     <xsl:variable name="fontsymbol">
40      <xsl:choose>
41       <xsl:when test="$symbol = 'leadsto'">
42        <xsl:value-of select="'&#174;'"/>
43       </xsl:when>
44       <xsl:when test="$symbol = 'sum'">
45        <xsl:value-of select="'&#229;'"/>
46       </xsl:when>
47       <xsl:otherwise>
48        <xsl:text>???</xsl:text>
49       </xsl:otherwise>
50      </xsl:choose>
51     </xsl:variable>
52     <FONT FACE="symbol" color="'blue'">
53      <xsl:value-of select="$fontsymbol"/>
54     </FONT>
55    </xsl:when>
56    <xsl:otherwise>
57     <xsl:variable name="unicodesymbol">
58      <xsl:choose>
59       <xsl:when test="$symbol = 'leadsto'">
60        <xsl:value-of select="'&#8594;'"/>
61       </xsl:when>
62       <xsl:when test="$symbol = 'sum'">
63        <xsl:value-of select="'&#x02211;'"/>
64       </xsl:when>
65       <xsl:otherwise>
66        <xsl:text>???</xsl:text>
67       </xsl:otherwise>
68      </xsl:choose>
69     </xsl:variable>
70     <FONT color="'blue'">
71      <xsl:value-of select="$unicodesymbol"/>
72     </FONT>
73    </xsl:otherwise>
74   </xsl:choose>
75 </xsl:template>
76
77 <!-- **************************************************************** -->
78 <!--                   INLINE MODE                                    -->
79 <!-- **************************************************************** -->
80
81 <!-- SUM -->
82
83 <xsl:template mode="inline" match="m:apply[m:sum]">
84      <xsl:variable name="uri">
85       <xsl:value-of select="m:sum/@definitionURL"/>
86      </xsl:variable>
87      <xsl:choose>
88       <xsl:when test="$uri != ''">
89        <a href="{$uri}">
90        <!-- 
91        <FONT FACE="symbol" color="'blue'">
92         <xsl:value-of select="'&#229;'"/>
93        </FONT> -->
94        <xsl:call-template name="mksymbol-reals">
95         <xsl:with-param name="symbol" select="'sum'"/>
96       </xsl:call-template>
97        </a>
98       </xsl:when>
99       <xsl:otherwise>
100        <!-- 
101        <FONT FACE="symbol" color="'blue'">
102         <xsl:value-of select="'&#229;'"/>
103        </FONT> -->
104        <xsl:call-template name="mksymbol-reals">
105         <xsl:with-param name="symbol" select="'sum'"/>
106        </xsl:call-template>
107       </xsl:otherwise>
108      </xsl:choose>
109      <xsl:choose>
110       <xsl:when test="m:condition">
111        <SUB>
112         <xsl:apply-templates select="m:condition"/>
113        </SUB>
114       </xsl:when>
115       <xsl:otherwise>
116        <SUB>
117         <xsl:apply-templates select="m:lowlimit/*[1]"/>
118         <xsl:call-template name="mksymbol-init">
119          <xsl:with-param name="symbol" select="'leq'"/>
120         </xsl:call-template>
121         <xsl:apply-templates select="m:bvar/*[1]"/>
122         <xsl:call-template name="mksymbol-init">
123          <xsl:with-param name="symbol" select="'leq'"/>
124         </xsl:call-template>
125         <xsl:apply-templates select="m:uplimit/*[1]"/>
126        </SUB>
127       </xsl:otherwise>
128      </xsl:choose>
129      <xsl:apply-templates mode="inline" select="*[position()=last()]"/>
130  </xsl:template>
131
132
133 <!-- LIMIT -->
134
135
136 <xsl:template mode="inline" match="m:apply[m:limit]">
137      <xsl:variable name="uri"><xsl:value-of select="m:limit/@definitionURL"/></xsl:variable>
138      <xsl:choose>
139      <xsl:when test="$uri != ''">
140       <a href="{$uri}">
141        <xsl:text>lim</xsl:text>
142       </a>
143      </xsl:when>
144      <xsl:otherwise>
145       <xsl:text>lim</xsl:text>
146      </xsl:otherwise>
147      </xsl:choose>
148      <SUB>
149       <xsl:apply-templates select="m:bvar/m:ci"/>
150       <xsl:call-template name="mksymbol-reals">
151        <xsl:with-param name="symbol" select="'leadsto'"/>
152       </xsl:call-template>
153       <xsl:apply-templates mode="inline" select="m:lowlimit"/>
154      </SUB>
155      <xsl:apply-templates mode="inline" select="*[4]"/>
156  </xsl:template>
157
158 <!-- DIFFERENTIATION -->
159
160 <xsl:template mode="inline" match="m:apply[m:diff]">
161      <xsl:variable name="uri"><xsl:value-of select="m:diff/@definitionURL"/></xsl:variable>
162      <xsl:choose>
163      <xsl:when test="$uri != ''">
164       <a href="{$uri}">
165        <SUP>d</SUP>
166        <xsl:text>/</xsl:text>
167        <SUB>
168         <xsl:text>d</xsl:text>
169         <xsl:value-of select="m:bvar/m:ci"/>
170        </SUB>
171       </a>
172      </xsl:when>
173      <xsl:otherwise>
174       <SUP>d</SUP>
175        <xsl:text>/</xsl:text>
176        <SUB>
177         <xsl:text>d</xsl:text>
178         <xsl:value-of select="m:bvar/m:ci"/>
179        </SUB>
180      </xsl:otherwise>
181      </xsl:choose>
182      <xsl:apply-templates mode="inline" select="*[3]"/>
183  </xsl:template>
184
185 <!-- ABSOLUTE VALUE -->
186 <xsl:template mode="inline" match="m:apply[m:abs]">
187   <xsl:variable name="uri">
188    <xsl:value-of select="m:abs/@definitionURL"/>
189   </xsl:variable>
190   <xsl:text>|</xsl:text>
191   <xsl:apply-templates mode="inline" select="*[2]"/>
192   <xsl:text>|</xsl:text>
193 </xsl:template>
194
195 <!-- FACTORIAL -->
196
197 <xsl:template mode="inline" match="m:apply[m:fact]">
198   <xsl:variable name="uri">
199    <xsl:value-of select="m:abs/@definitionURL"/>
200   </xsl:variable>
201   <xsl:apply-templates mode="inline" select="*[2]"/>
202   <xsl:text>!</xsl:text>
203 </xsl:template>
204
205 <!-- SQUARE ROOT -->
206
207 <xsl:template match="m:apply[m:root]">
208   <xsl:variable name="uri">
209    <xsl:value-of select="m:abs/@definitionURL"/>
210   </xsl:variable>
211   <xsl:text>(sqr</xsl:text>
212   <xsl:apply-templates mode="inline" select="*[2]"/>
213   <xsl:text>)</xsl:text>
214 </xsl:template>
215
216 <!-- POWER -->
217
218 <xsl:template mode="inline" match="m:apply[m:power]">
219   <xsl:variable name="uri">
220    <xsl:value-of select="m:power/@definitionURL"/>
221   </xsl:variable>
222   <xsl:apply-templates mode="inline" select="*[2]"/>
223   <SUP>
224   <xsl:apply-templates mode="inline" select="*[3]"/>
225   </SUP>
226 </xsl:template>
227
228 <!-- MIN and MAX (binari: estendere) -->
229
230  <xsl:template mode="inline" match="m:apply[m:min|m:max]">
231   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
232   <xsl:variable name="symbol">
233    <xsl:choose>
234     <xsl:when test="m:min">
235      <xsl:value-of select="'min'"/>
236     </xsl:when>
237     <xsl:when test="m:max">
238      <xsl:value-of select="'max'"/>
239     </xsl:when>
240    </xsl:choose>
241   </xsl:variable>
242   <xsl:choose>
243   <xsl:when test="$uri != ''">
244    <a href="{$uri}">
245     <xsl:value-of select="$symbol"/>
246    </a>
247   </xsl:when>
248   <xsl:otherwise>
249    <xsl:value-of select="$symbol"/>
250   </xsl:otherwise>
251   </xsl:choose>
252   <xsl:text>{</xsl:text>
253   <xsl:apply-templates mode="inline" select="*[2]"/>
254   <xsl:text>, </xsl:text>
255   <xsl:apply-templates mode="inline" select="*[3]"/>
256   <xsl:text>}</xsl:text>
257 </xsl:template>
258
259 <!-- **************************************************************** -->
260 <!--                   COUNTING MODE                                    -->
261 <!-- **************************************************************** -->
262
263 <xsl:template match="m:apply[m:sum]">
264  <xsl:apply-templates mode="inline" select="."/>
265 </xsl:template>
266
267 <xsl:template match="m:apply[m:limit]">
268   <xsl:param name="current_indent" select="0"/> 
269   <xsl:param name="width" select="$framewidth"/>
270   <xsl:variable name="uri"><xsl:value-of select="m:limit/@definitionURL"/></xsl:variable>
271   <xsl:variable name="charlength">
272    <xsl:apply-templates select="m:limit" mode="charcount"/>
273   </xsl:variable>
274   <xsl:choose>
275     <xsl:when test="$charlength > $framewidth">
276      <xsl:choose>
277      <xsl:when test="$uri != ''">
278       <a href="{$uri}">
279        <xsl:text>lim</xsl:text>
280       </a>
281      </xsl:when>
282      <xsl:otherwise>
283       <xsl:text>lim</xsl:text>
284      </xsl:otherwise>
285      </xsl:choose>
286      <SUB>
287       <xsl:apply-templates select="m:bvar/m:ci"/>
288       <xsl:call-template name="mksymbol-reals">
289        <xsl:with-param name="symbol" select="'leadsto'"/>
290       </xsl:call-template>
291       <xsl:apply-templates select="m:lowlimit"/>
292      </SUB>
293      <BR/> 
294      <xsl:call-template name="make_indent">
295       <xsl:with-param name="current_indent" select="$current_indent + 5"/> 
296      </xsl:call-template>
297      <xsl:apply-templates select="*[4]">
298       <xsl:with-param name="current_indent" select="$current_indent + 5"/>
299      </xsl:apply-templates>
300     </xsl:when>
301     <xsl:otherwise>
302      <xsl:apply-templates mode="inline" select="."/>
303     </xsl:otherwise>
304    </xsl:choose>
305  </xsl:template>
306
307 <!-- DIFFERENTIATION -->
308 <xsl:template match="m:apply[m:diff]">
309   <xsl:param name="current_indent" select="0"/> 
310   <xsl:param name="width" select="$framewidth"/>
311   <xsl:variable name="uri"><xsl:value-of select="m:diff/@definitionURL"/></xsl:variable>
312      <xsl:choose>
313      <xsl:when test="$uri != ''">
314       <a href="{$uri}">
315        <SUP>d</SUP>
316        <xsl:text>/</xsl:text>
317        <SUB>
318         <xsl:text>d</xsl:text>
319         <xsl:value-of select="m:bvar/m:ci"/>
320        </SUB>
321       </a>
322      </xsl:when>
323      <xsl:otherwise>
324        <SUP>d</SUP>
325        <xsl:text>/</xsl:text>
326        <SUB>
327         <xsl:text>d</xsl:text>
328         <xsl:value-of select="m:bvar/m:ci"/>
329        </SUB>
330      </xsl:otherwise>
331      </xsl:choose>
332      <xsl:apply-templates select="*[3]">
333       <xsl:with-param name="current_indent" select="$current_indent + 5"/>
334      </xsl:apply-templates>
335  </xsl:template>
336
337
338 <!-- ABSOLUTE VALUE -->
339 <xsl:template match="m:apply[m:abs]">
340   <xsl:param name="current_indent" select="0"/> 
341   <xsl:param name="width" select="$framewidth"/>
342   <xsl:variable name="uri">
343    <xsl:value-of select="m:abs/@definitionURL"/>
344   </xsl:variable>
345   <xsl:text>|</xsl:text>
346   <xsl:apply-templates select="*[2]">
347    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
348   </xsl:apply-templates>
349   <xsl:text>|</xsl:text>
350  </xsl:template>
351
352 <!-- FACTORIAL -->
353
354 <xsl:template match="m:apply[m:fact]">
355   <xsl:param name="current_indent" select="0"/> 
356   <xsl:param name="width" select="$framewidth"/>
357   <xsl:variable name="uri">
358    <xsl:value-of select="m:abs/@definitionURL"/>
359   </xsl:variable>
360   <xsl:apply-templates select="*[2]">
361    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
362   </xsl:apply-templates>
363   <xsl:text>!</xsl:text>
364  </xsl:template>
365
366 <!-- SQUARE ROOT -->
367
368 <xsl:template match="m:apply[m:root]">
369   <xsl:param name="current_indent" select="0"/> 
370   <xsl:param name="width" select="$framewidth"/>
371   <xsl:variable name="uri">
372    <xsl:value-of select="m:abs/@definitionURL"/>
373   </xsl:variable>
374   <xsl:text>(sqr</xsl:text>
375   <xsl:apply-templates select="*[2]">
376    <xsl:with-param name="current_indent" select="$current_indent + 5"/>
377   </xsl:apply-templates>
378   <xsl:text>)</xsl:text>
379  </xsl:template>
380
381 <!-- POWER -->
382
383 <xsl:template match="m:apply[m:power]">
384   <xsl:param name="current_indent" select="0"/> 
385   <xsl:param name="width" select="$framewidth"/>
386   <xsl:variable name="uri">
387    <xsl:value-of select="m:power/@definitionURL"/>
388   </xsl:variable>
389   <xsl:apply-templates select="*[2]"/>
390   <SUP>
391   <xsl:apply-templates select="*[3]"/>
392   </SUP>
393  </xsl:template>
394
395 <!-- MIN and MAX (binari: estendere) -->
396
397  <xsl:template match="m:apply[m:min|m:max]">
398   <xsl:param name="current_indent" select="0"/> 
399   <xsl:param name="width" select="$framewidth"/>
400   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
401   <xsl:variable name="charlength">
402    <xsl:apply-templates select="*[1]" mode="charcount"/>
403   </xsl:variable>
404   <xsl:variable name="symbol">
405    <xsl:choose>
406     <xsl:when test="m:min">
407      <xsl:value-of select="'min'"/>
408     </xsl:when>
409     <xsl:when test="m:max">
410      <xsl:value-of select="'max'"/>
411     </xsl:when>
412    </xsl:choose>
413   </xsl:variable>
414   <xsl:choose>
415     <xsl:when test="$charlength > $framewidth">
416      <xsl:choose>
417      <xsl:when test="$uri != ''">
418       <a href="{$uri}">
419        <xsl:value-of select="$symbol"/>
420       </a>
421      </xsl:when>
422      <xsl:otherwise>
423       <xsl:value-of select="$symbol"/>
424      </xsl:otherwise>
425      </xsl:choose>
426      <xsl:text>{</xsl:text>
427      <xsl:apply-templates select="*[2]">
428       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
429      </xsl:apply-templates>
430      <xsl:text>,</xsl:text>
431      <BR/> 
432      <xsl:call-template name="make_indent">
433       <xsl:with-param name="current_indent" select="$current_indent + 5"/> 
434      </xsl:call-template>
435      <xsl:apply-templates select="*[3]">
436       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
437      </xsl:apply-templates>
438      <xsl:text>}</xsl:text>
439     </xsl:when>
440     <xsl:otherwise>
441      <xsl:apply-templates mode="inline" select="."/>
442     </xsl:otherwise>
443    </xsl:choose>
444  </xsl:template>
445
446 <!-- COUNTING -->
447
448 <xsl:template match="m:abs|m:fact|m:root|
449            m:sum|m:limit|m:diff|m:min|m:max" mode="charcount">
450 <xsl:param name="incurrent_length" select="0"/> 
451     <xsl:choose>
452     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
453      <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>
454      <xsl:choose>
455      <xsl:when test="string($siblength) = &quot;&quot;">
456       <xsl:value-of select="$incurrent_length + string-length()"/>
457      </xsl:when>
458      <xsl:otherwise>
459       <xsl:value-of select="number($siblength)"/>
460      </xsl:otherwise>
461      </xsl:choose>
462     </xsl:when>
463     <xsl:otherwise>
464      <xsl:value-of select="$incurrent_length + string-length()"/>
465     </xsl:otherwise>
466     </xsl:choose>
467 </xsl:template> 
468
469 </xsl:stylesheet>