]> matita.cs.unibo.it Git - helm.git/blob - helm/style/html_reals.xsl
Requires and Provides now fixed
[helm.git] / helm / style / html_reals.xsl
1 <?xml version="1.0"?>
2
3 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
4                               xmlns:m="http://www.w3.org/1998/Math/MathML">
5
6 <!--***********************************************************************--> 
7 <!-- INIT style for HTML                                                   -->
8 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
9 <!--***********************************************************************--> 
10
11 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
12
13 <!-- LIMIT -->
14
15 <xsl:template match="m:apply[m:limit]">
16   <xsl:param name="current_indent" select="0"/> 
17   <xsl:param name="width" select="$framewidth"/>
18   <xsl:variable name="uri">
19    <xsl:value-of select="m:limit/@definitionURL"/>
20   </xsl:variable>
21   <xsl:variable name="charlength">
22    <xsl:apply-templates select="m:limit" mode="charcount"/>
23   </xsl:variable>
24   <xsl:choose>
25     <xsl:when test="$charlength > $framewidth">
26      <a>
27      <xsl:attribute name="href">
28       <xsl:value-of select="concat(string($header),string($uri))"/>
29      </xsl:attribute>
30      <xsl:text>lim</xsl:text>
31      </a>
32      <SUB>
33       <xsl:apply-templates select="m:bvar/m:ci"/>
34       <FONT FACE="symbol" color="blue">&#174;</FONT>
35       <xsl:apply-templates select="m:lowlimit"/>
36      </SUB>
37      <BR/> 
38      <xsl:call-template name="make_indent">
39       <xsl:with-param name="current_indent" select="$current_indent + 5"/> 
40      </xsl:call-template>
41      <xsl:apply-templates select="*[4]">
42       <xsl:with-param name="current_indent" select="$current_indent + 5"/>
43      </xsl:apply-templates>
44     </xsl:when>
45     <xsl:otherwise>
46      <a>
47      <xsl:attribute name="href">
48       <xsl:value-of select="concat(string($header),string($uri))"/>
49      </xsl:attribute>
50      <xsl:text>lim</xsl:text>
51      </a>
52      <SUB>
53       <xsl:apply-templates select="m:bvar/m:ci"/>
54       <FONT FACE="symbol" color="blue">&#174;</FONT>
55       <xsl:apply-templates select="m:lowlimit"/>
56      </SUB>
57      <xsl:apply-templates select="*[4]">
58       <xsl:with-param name="current_indent" select="$current_indent + 5"/>
59      </xsl:apply-templates>
60     </xsl:otherwise>
61    </xsl:choose>
62  </xsl:template>
63
64 <!-- DIFFERENTIATION -->
65
66 <xsl:template match="m:apply[m:diff]">
67   <xsl:param name="current_indent" select="0"/> 
68   <xsl:param name="width" select="$framewidth"/>
69   <xsl:variable name="uri">
70    <xsl:value-of select="m:diff/@definitionURL"/>
71   </xsl:variable>
72      <a>
73      <xsl:attribute name="href">
74       <xsl:value-of select="concat(string($header),string($uri))"/>
75      </xsl:attribute>
76      <SUP>d</SUP>
77       <xsl:text>/</xsl:text>
78      <SUB>
79       <xsl:text>d</xsl:text>
80       <xsl:value-of select="m:bvar/m:ci"/>
81      </SUB>
82      </a>
83      <xsl:apply-templates select="*[3]">
84       <xsl:with-param name="current_indent" select="$current_indent + 5"/>
85      </xsl:apply-templates>
86  </xsl:template>
87
88 <!-- ABSOLUTE VALUE -->
89 <xsl:template match="m:apply[m:abs]">
90   <xsl:param name="current_indent" select="0"/> 
91   <xsl:param name="width" select="$framewidth"/>
92   <xsl:variable name="uri">
93    <xsl:value-of select="m:abs/@definitionURL"/>
94   </xsl:variable>
95   <xsl:text>|</xsl:text>
96   <xsl:apply-templates select="*[2]">
97    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
98   </xsl:apply-templates>
99   <xsl:text>|</xsl:text>
100  </xsl:template>
101
102 <!-- FACTORIAL -->
103
104 <xsl:template match="m:apply[m:fact]">
105   <xsl:param name="current_indent" select="0"/> 
106   <xsl:param name="width" select="$framewidth"/>
107   <xsl:variable name="uri">
108    <xsl:value-of select="m:abs/@definitionURL"/>
109   </xsl:variable>
110   <xsl:apply-templates select="*[2]">
111    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
112   </xsl:apply-templates>
113   <xsl:text>!</xsl:text>
114  </xsl:template>
115
116 <!-- SQUARE ROOT -->
117
118 <xsl:template match="m:apply[m:root]">
119   <xsl:param name="current_indent" select="0"/> 
120   <xsl:param name="width" select="$framewidth"/>
121   <xsl:variable name="uri">
122    <xsl:value-of select="m:abs/@definitionURL"/>
123   </xsl:variable>
124   <xsl:text>(sqr</xsl:text>
125   <xsl:apply-templates select="*[2]">
126    <xsl:with-param name="current_indent" select="$current_indent + 5"/>
127   </xsl:apply-templates>
128   <xsl:text>)</xsl:text>
129  </xsl:template>
130
131 <!-- POWER -->
132
133 <xsl:template match="m:apply[m:power]">
134   <xsl:param name="current_indent" select="0"/> 
135   <xsl:param name="width" select="$framewidth"/>
136   <xsl:variable name="uri">
137    <xsl:value-of select="m:power/@definitionURL"/>
138   </xsl:variable>
139   <xsl:apply-templates select="*[2]"/>
140   <SUP>
141   <xsl:apply-templates select="*[3]"/>
142   </SUP>
143  </xsl:template>
144
145 <!-- MIN and MAX (binari: estendere) -->
146
147  <xsl:template match="m:apply[m:min|m:max]">
148   <xsl:param name="current_indent" select="0"/> 
149   <xsl:param name="width" select="$framewidth"/>
150   <xsl:variable name="uri">
151    <xsl:value-of select="*[1]/@definitionURL"/>
152   </xsl:variable>
153   <xsl:variable name="charlength">
154    <xsl:apply-templates select="*[1]" mode="charcount"/>
155   </xsl:variable>
156   <xsl:variable name="symbol">
157    <xsl:choose>
158     <xsl:when test="m:min">
159      <xsl:value-of select="'min'"/>
160     </xsl:when>
161     <xsl:when test="m:max">
162      <xsl:value-of select="'max'"/>
163     </xsl:when>
164    </xsl:choose>
165   </xsl:variable>
166   <xsl:choose>
167     <xsl:when test="$charlength > $framewidth">
168      <a>
169      <xsl:attribute name="href">
170       <xsl:value-of select="concat(string($header),string($uri))"/>
171      </xsl:attribute>
172      <xsl:value-of select="$symbol"/>
173      </a>
174      <xsl:text>{</xsl:text>
175      <xsl:apply-templates select="*[2]">
176       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
177      </xsl:apply-templates>
178      <xsl:text>,</xsl:text>
179      <BR/> 
180      <xsl:call-template name="make_indent">
181       <xsl:with-param name="current_indent" select="$current_indent + 5"/> 
182      </xsl:call-template>
183      <xsl:apply-templates select="*[3]">
184       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
185      </xsl:apply-templates>
186      <xsl:text>}</xsl:text>
187     </xsl:when>
188     <xsl:otherwise>
189      <a>
190      <xsl:attribute name="href">
191       <xsl:value-of select="concat(string($header),string($uri))"/>
192      </xsl:attribute>
193      <xsl:value-of select="$symbol"/>
194      </a>
195      <xsl:text>{</xsl:text>
196      <xsl:apply-templates select="*[2]"/>
197      <xsl:text>, </xsl:text>
198      <xsl:apply-templates select="*[3]"/>
199      <xsl:text>}</xsl:text>
200     </xsl:otherwise>
201    </xsl:choose>
202  </xsl:template>
203
204 <!-- COUNTING -->
205
206 <xsl:template match="m:abs|m:fact|m:root
207            |m:limit|m:diff|m:min|m:max" mode="charcount">
208 <xsl:param name="incurrent_length" select="0"/> 
209     <xsl:choose>
210     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
211      <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>
212      <xsl:choose>
213      <xsl:when test="string($siblength) = &quot;&quot;">
214       <xsl:value-of select="$incurrent_length + string-length()"/>
215      </xsl:when>
216      <xsl:otherwise>
217       <xsl:value-of select="number($siblength)"/>
218      </xsl:otherwise>
219      </xsl:choose>
220     </xsl:when>
221     <xsl:otherwise>
222      <xsl:value-of select="$incurrent_length + string-length()"/>
223     </xsl:otherwise>
224     </xsl:choose>
225 </xsl:template> 
226
227 </xsl:stylesheet> 
228
229
230
231
232
233
234