3 <!-- Copyright (C) 2000, HELM Team -->
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. -->
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. -->
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. -->
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. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
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">
30 <!--***********************************************************************-->
31 <!-- INIT style for HTML -->
32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
33 <!--***********************************************************************-->
35 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
39 <xsl:template match="m:apply[m:in]">
40 <xsl:param name="current_indent" select="0"/>
41 <xsl:param name="width" select="$framewidth"/>
42 <xsl:variable name="uri">
43 <xsl:value-of select="m:in/@definitionURL"/>
45 <xsl:variable name="charlength">
46 <xsl:apply-templates select="m:in" mode="charcount"/>
49 <xsl:when test="$charlength > $framewidth">
50 <xsl:text>(</xsl:text>
51 <xsl:apply-templates select="*[2]">
52 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
53 </xsl:apply-templates>
55 <xsl:call-template name="make_indent">
56 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
59 <xsl:attribute name="href">
60 <xsl:value-of select="concat(string($header),string($uri))"/>
62 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Î</FONT>
64 <xsl:apply-templates select="*[3]">
65 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
66 </xsl:apply-templates>
67 <xsl:text>)</xsl:text>
70 <xsl:text>(</xsl:text>
71 <xsl:apply-templates select="*[2]"/>
73 <xsl:attribute name="href">
74 <xsl:value-of select="concat(string($header),string($uri))"/>
76 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Î</FONT>
78 <xsl:apply-templates select="*[3]"/>
79 <xsl:text>)</xsl:text>
86 <xsl:template match="m:apply[m:notin]">
87 <xsl:param name="current_indent" select="0"/>
88 <xsl:param name="width" select="$framewidth"/>
89 <xsl:variable name="uri">
90 <xsl:value-of select="m:notin/@definitionURL"/>
92 <xsl:variable name="charlength">
93 <xsl:apply-templates select="m:notin" mode="charcount"/>
96 <xsl:when test="$charlength > $framewidth">
97 <xsl:text>(</xsl:text>
98 <xsl:apply-templates select="*[2]">
99 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
100 </xsl:apply-templates>
102 <xsl:call-template name="make_indent">
103 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
105 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ï</FONT>
106 <xsl:apply-templates select="*[3]">
107 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
108 </xsl:apply-templates>
109 <xsl:text>)</xsl:text>
112 <xsl:text>(</xsl:text>
113 <xsl:apply-templates select="*[2]"/>
114 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ï</FONT>
115 <xsl:apply-templates select="*[3]"/>
116 <xsl:text>)</xsl:text>
123 <xsl:template match="m:set">
124 <xsl:param name="current_indent" select="0"/>
125 <xsl:param name="width" select="$framewidth"/>
126 <xsl:variable name="uri">
127 <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
130 <xsl:when test="count(child::*) = 0">
131 <FONT FACE="symbol" mathcolor="blue">Æ</FONT>
134 <xsl:variable name="charlength">
135 <xsl:apply-templates select="." mode="charcount"/>
138 <xsl:when test="name(*[1]) = 'm:bvar'">
140 <xsl:when test="$charlength > $framewidth">
141 <xsl:text>{</xsl:text>
142 <xsl:apply-templates select="m:bvar/m:ci"/>
143 <xsl:text>:</xsl:text>
144 <xsl:apply-templates select="m:bvar/m:type">
145 <xsl:with-param name="current_indent"
146 select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
147 </xsl:apply-templates><BR/>
148 <xsl:call-template name="make_indent">
149 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
151 <xsl:text>|</xsl:text>
152 <xsl:apply-templates select="m:condition">
153 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
154 </xsl:apply-templates>
155 <xsl:text>}</xsl:text>
158 <xsl:text>{</xsl:text>
159 <xsl:apply-templates select="m:bvar/m:ci"/>
160 <xsl:text>:</xsl:text>
161 <xsl:apply-templates select="m:bvar/m:type"/>
162 <xsl:text>|</xsl:text>
163 <xsl:apply-templates select="*[position()=2]"/>
164 <xsl:text>}</xsl:text>
170 <xsl:when test="$charlength > $framewidth">
171 <xsl:text>{</xsl:text>
172 <xsl:apply-templates select="*[position()=1]">
173 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
174 </xsl:apply-templates>
175 <xsl:for-each select="*[position()>1]">
176 <xsl:text>,</xsl:text>
178 <xsl:call-template name="make_indent">
179 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
181 <xsl:apply-templates select=".">
182 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
183 </xsl:apply-templates>
185 <xsl:text>}</xsl:text>
188 <xsl:text>{</xsl:text>
189 <xsl:for-each select="*">
190 <xsl:apply-templates select="."/>
192 <xsl:when test="position() = last()">
193 <xsl:text>}</xsl:text>
196 <xsl:text>,</xsl:text>
209 <!-- INTERSECTION -->
211 <xsl:template match="m:apply[m:intersect]">
212 <xsl:param name="current_indent" select="0"/>
213 <xsl:param name="width" select="$framewidth"/>
214 <xsl:variable name="uri">
215 <xsl:value-of select="m:intersect/@definitionURL"/>
217 <xsl:variable name="charlength">
218 <xsl:apply-templates select="m:intersect" mode="charcount"/>
221 <xsl:when test="$charlength > $framewidth">
222 <xsl:text>(</xsl:text>
223 <xsl:apply-templates select="*[2]">
224 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
225 </xsl:apply-templates>
227 <xsl:call-template name="make_indent">
228 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
231 <xsl:attribute name="href">
232 <xsl:value-of select="concat(string($header),string($uri))"/>
234 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ç</FONT>
236 <xsl:apply-templates select="*[3]">
237 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
238 </xsl:apply-templates>
239 <xsl:text>)</xsl:text>
242 <xsl:text>(</xsl:text>
243 <xsl:apply-templates select="*[2]"/>
245 <xsl:attribute name="href">
246 <xsl:value-of select="concat(string($header),string($uri))"/>
248 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ç</FONT>
250 <xsl:apply-templates select="*[3]"/>
251 <xsl:text>)</xsl:text>
258 <xsl:template match="m:apply[m:union]">
259 <xsl:param name="current_indent" select="0"/>
260 <xsl:param name="width" select="$framewidth"/>
261 <xsl:variable name="uri">
262 <xsl:value-of select="m:union/@definitionURL"/>
264 <xsl:variable name="charlength">
265 <xsl:apply-templates select="m:union" mode="charcount"/>
268 <xsl:when test="$charlength > $framewidth">
269 <xsl:text>(</xsl:text>
270 <xsl:apply-templates select="*[2]">
271 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
272 </xsl:apply-templates>
274 <xsl:call-template name="make_indent">
275 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
278 <xsl:attribute name="href">
279 <xsl:value-of select="concat(string($header),string($uri))"/>
281 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">È</FONT>
283 <xsl:apply-templates select="*[3]">
284 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
285 </xsl:apply-templates>
286 <xsl:text>)</xsl:text>
289 <xsl:text>(</xsl:text>
290 <xsl:apply-templates select="*[2]"/>
292 <xsl:attribute name="href">
293 <xsl:value-of select="concat(string($header),string($uri))"/>
295 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">È</FONT>
297 <xsl:apply-templates select="*[3]"/>
298 <xsl:text>)</xsl:text>
304 <xsl:template match="m:apply[m:subset]">
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:subset/@definitionURL"/>
310 <xsl:variable name="charlength">
311 <xsl:apply-templates select="m:subset" mode="charcount"/>
314 <xsl:when test="$charlength > $framewidth">
315 <xsl:text>(</xsl:text>
316 <xsl:apply-templates select="*[2]">
317 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
318 </xsl:apply-templates>
320 <xsl:call-template name="make_indent">
321 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
324 <xsl:attribute name="href">
325 <xsl:value-of select="concat(string($header),string($uri))"/>
327 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Í</FONT>
329 <xsl:apply-templates select="*[3]">
330 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
331 </xsl:apply-templates>
332 <xsl:text>)</xsl:text>
335 <xsl:text>(</xsl:text>
336 <xsl:apply-templates select="*[2]"/>
338 <xsl:attribute name="href">
339 <xsl:value-of select="concat(string($header),string($uri))"/>
341 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Í</FONT>
343 <xsl:apply-templates select="*[3]"/>
344 <xsl:text>)</xsl:text>
350 <xsl:template match="m:apply[m:prsubset]">
351 <xsl:param name="current_indent" select="0"/>
352 <xsl:param name="width" select="$framewidth"/>
353 <xsl:variable name="uri">
354 <xsl:value-of select="m:prsubset/@definitionURL"/>
356 <xsl:variable name="charlength">
357 <xsl:apply-templates select="m:prsubset" mode="charcount"/>
360 <xsl:when test="$charlength > $framewidth">
361 <xsl:text>(</xsl:text>
362 <xsl:apply-templates select="*[2]">
363 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
364 </xsl:apply-templates>
366 <xsl:call-template name="make_indent">
367 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
370 <xsl:attribute name="href">
371 <xsl:value-of select="concat(string($header),string($uri))"/>
373 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ì</FONT>
375 <xsl:apply-templates select="*[3]">
376 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
377 </xsl:apply-templates>
378 <xsl:text>)</xsl:text>
381 <xsl:text>(</xsl:text>
382 <xsl:apply-templates select="*[2]"/>
384 <xsl:attribute name="href">
385 <xsl:value-of select="concat(string($header),string($uri))"/>
387 <FONT FACE="symbol" SIZE="+2" mathcolor="blue">Ì</FONT>
389 <xsl:apply-templates select="*[3]"/>
390 <xsl:text>)</xsl:text>
398 <xsl:template match="m:apply[m:setdiff]">
399 <xsl:param name="current_indent" select="0"/>
400 <xsl:param name="width" select="$framewidth"/>
401 <xsl:variable name="uri">
402 <xsl:value-of select="m:setdiff/@definitionURL"/>
404 <xsl:variable name="charlength">
405 <xsl:apply-templates select="m:setdiff" mode="charcount"/>
408 <xsl:when test="$charlength > $framewidth">
409 <xsl:text>(</xsl:text>
410 <xsl:apply-templates select="*[2]">
411 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
412 </xsl:apply-templates>
414 <xsl:call-template name="make_indent">
415 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
418 <xsl:attribute name="href">
419 <xsl:value-of select="concat(string($header),string($uri))"/>
421 <xsl:text>/</xsl:text>
423 <xsl:apply-templates select="*[3]">
424 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
425 </xsl:apply-templates>
426 <xsl:text>)</xsl:text>
429 <xsl:text>(</xsl:text>
430 <xsl:apply-templates select="*[2]"/>
432 <xsl:attribute name="href">
433 <xsl:value-of select="concat(string($header),string($uri))"/>
435 <xsl:text>/</xsl:text>
437 <xsl:apply-templates select="*[3]"/>
438 <xsl:text>)</xsl:text>
444 <xsl:template match="m:apply[m:card]">
445 <xsl:param name="current_indent" select="0"/>
446 <xsl:param name="width" select="$framewidth"/>
447 <xsl:variable name="uri">
448 <xsl:value-of select="m:card/@definitionURL"/>
450 <xsl:text>|</xsl:text>
451 <xsl:apply-templates select="*[2]">
452 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
453 </xsl:apply-templates>
454 <xsl:text>|</xsl:text>
459 <xsl:template match="m:in|m:notin|m:intersect|m:union
460 |m:subset|m:prsubset|m:setdiff|m:card" mode="charcount">
461 <xsl:param name="incurrent_length" select="0"/>
463 <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
464 <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>
466 <xsl:when test="string($siblength) = """>
467 <xsl:value-of select="$incurrent_length + string-length()"/>
470 <xsl:value-of select="number($siblength)"/>
475 <xsl:value-of select="$incurrent_length + string-length()"/>