]> matita.cs.unibo.it Git - helm.git/blob - helm/style/html_set.xsl
UNICODEvsSYMBOL introduced everywhere. (work completed)
[helm.git] / helm / style / html_set.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">
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 = 'emptyset'">
42        <xsl:value-of select="'&#198;'"/>
43       </xsl:when>
44       <xsl:when test="$symbol = 'in'">
45        <xsl:value-of select="'&#206;'"/>
46       </xsl:when>
47       <xsl:when test="$symbol = 'notin'">
48        <xsl:value-of select="'&#207;'"/>
49       </xsl:when>
50       <xsl:when test="$symbol = 'intersect'">
51        <xsl:value-of select="'&#199;'"/>
52       </xsl:when>
53       <xsl:when test="$symbol = 'union'">
54        <xsl:value-of select="'&#200;'"/>
55       </xsl:when>
56       <xsl:when test="$symbol = 'subset'">
57        <xsl:value-of select="'&#205;'"/>
58       </xsl:when>
59       <xsl:when test="$symbol = 'prsubset'">
60        <xsl:value-of select="'&#204;'"/>
61       </xsl:when>
62       <xsl:when test="$symbol = 'setdiff'">
63        <xsl:value-of select="'/'"/>
64       </xsl:when>
65      </xsl:choose>
66     </xsl:variable>
67     <FONT FACE="symbol" mathcolor="blue">
68      <xsl:value-of select="$fontsymbol"/>
69     </FONT>
70    </xsl:when>
71    <xsl:otherwise>
72     <xsl:variable name="unicodesymbol">
73      <xsl:choose>
74       <xsl:when test="$symbol = 'emptyset'">
75        <xsl:value-of select="'&#8709;'"/>
76       </xsl:when>
77       <xsl:when test="$symbol = 'in'">
78        <xsl:value-of select="'&#8712;'"/>
79       </xsl:when>
80       <xsl:when test="$symbol = 'notin'">
81        <xsl:value-of select="'&#8713;'"/>
82       </xsl:when>
83       <xsl:when test="$symbol = 'intersect'">
84        <xsl:value-of select="'&#8745;'"/>
85       </xsl:when>
86       <xsl:when test="$symbol = 'union'">
87        <xsl:value-of select="'&#8746;'"/>
88       </xsl:when>
89       <xsl:when test="$symbol = 'subset'">
90        <xsl:value-of select="'&#8838;'"/>
91       </xsl:when>
92       <xsl:when test="$symbol = 'prsubset'">
93        <xsl:value-of select="'&#8834;'"/>
94       </xsl:when>
95       <xsl:when test="$symbol = 'setdiff'">
96        <xsl:value-of select="'&#47;'"/>
97       </xsl:when>
98      </xsl:choose>
99     </xsl:variable>
100     <xsl:value-of select="$unicodesymbol"/>
101    </xsl:otherwise>
102   </xsl:choose>
103 </xsl:template>
104
105 <!-- **************************************************************** -->
106 <!--                   INLINE MODE                                    -->
107 <!-- **************************************************************** -->
108
109 <!-- SET -->
110
111  <xsl:template mode="inline" match="m:set">
112   <xsl:variable name="uri" select="@definitionURL"/>
113 <!--   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
114   </xsl:variable>-->
115   <xsl:choose>
116    <xsl:when test="count(child::*) = 0">
117     <xsl:call-template name="mksymbol">
118      <xsl:with-param name="symbol" select="'emptyset'"/>
119     </xsl:call-template>
120    </xsl:when>
121    <xsl:otherwise>
122     <xsl:choose>
123      <xsl:when test="name(*[1]) = 'm:bvar'">
124       <xsl:text>{</xsl:text>
125       <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
126       <xsl:text>:</xsl:text>
127       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
128       <xsl:text>|</xsl:text>
129       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
130       <xsl:text>}</xsl:text>
131      </xsl:when>
132      <xsl:otherwise>
133       <xsl:text>{</xsl:text>
134       <xsl:for-each select="*">
135        <xsl:apply-templates mode="inline" select="."/>
136        <xsl:choose>
137         <xsl:when test="position() = last()">
138          <xsl:text>}</xsl:text>
139         </xsl:when>
140         <xsl:otherwise>
141          <xsl:text>,</xsl:text>
142         </xsl:otherwise>
143        </xsl:choose>
144       </xsl:for-each>
145      </xsl:otherwise>
146     </xsl:choose>
147    </xsl:otherwise>
148   </xsl:choose>
149  </xsl:template>
150
151
152 <!-- CARD -->
153 <xsl:template mode="inline" match="m:apply[m:card]">
154   <xsl:param name="current_indent" select="0"/> 
155   <xsl:param name="width" select="$framewidth"/>
156   <xsl:variable name="uri">
157    <xsl:value-of select="m:card/@definitionURL"/>
158   </xsl:variable>
159   <xsl:text>|</xsl:text>
160   <xsl:apply-templates mode="inline" select="*[2]"/>
161   <xsl:text>|</xsl:text>
162  </xsl:template>
163
164 <xsl:template mode="inline" match="m:apply[m:in|m:notin|m:intersect|m:union
165   |m:subset|m:prsubset|m:setdiff]">
166   <xsl:variable name="uri">
167    <xsl:value-of select="*[1]/@definitionURL"/>
168   </xsl:variable>
169   <xsl:variable name="symbol">
170    <xsl:choose>
171     <xsl:when test="m:in">
172      <xsl:value-of select="'&#206;'"/>
173     </xsl:when>
174     <xsl:when test="m:notin">
175      <xsl:value-of select="'&#207;'"/>
176     </xsl:when>
177     <xsl:when test="m:intersect">
178      <xsl:value-of select="'&#199;'"/>
179     </xsl:when>
180     <xsl:when test="m:union">
181      <xsl:value-of select="'&#200;'"/>
182     </xsl:when>
183     <xsl:when test="m:subset">
184      <xsl:value-of select="'&#205;'"/>
185     </xsl:when>
186     <xsl:when test="m:prsubset">
187      <xsl:value-of select="'&#204;'"/>
188     </xsl:when>
189     <xsl:when test="m:setdiff">
190      <xsl:value-of select="'/'"/>
191     </xsl:when>
192    </xsl:choose>
193   </xsl:variable>
194   <xsl:text>(</xsl:text>
195   <xsl:apply-templates mode="inline" select="*[2]"/>
196   <a href="{$uri}">
197    <xsl:call-template name="mksymbol">
198     <xsl:with-param name="symbol">
199      <xsl:value-of select="local-name(*[1])"/>
200     </xsl:with-param>
201    </xsl:call-template>
202   </a>
203   <xsl:apply-templates mode="inline" select="*[3]"/>
204   <xsl:text>)</xsl:text>
205  </xsl:template>
206
207 <!-- *************************************************************** -->
208
209 <xsl:template match="m:apply[m:in|m:notin|m:intersect|m:union
210   |m:subset|m:prsubset|m:setdiff]">
211   <xsl:param name="current_indent" select="0"/> 
212   <xsl:param name="width" select="$framewidth"/>
213   <xsl:variable name="uri">
214    <xsl:value-of select="*[1]/@definitionURL"/>
215   </xsl:variable>
216   <xsl:variable name="charlength">
217    <xsl:apply-templates select="*[1]" mode="charcount"/>
218   </xsl:variable>
219   <xsl:variable name="symbol">
220    <xsl:choose>
221     <xsl:when test="m:in">
222      <xsl:value-of select="'&#206;'"/>
223     </xsl:when>
224     <xsl:when test="m:notin">
225      <xsl:value-of select="'&#207;'"/>
226     </xsl:when>
227     <xsl:when test="m:intersect">
228      <xsl:value-of select="'&#199;'"/>
229     </xsl:when>
230     <xsl:when test="m:union">
231      <xsl:value-of select="'&#200;'"/>
232     </xsl:when>
233     <xsl:when test="m:subset">
234      <xsl:value-of select="'&#205;'"/>
235     </xsl:when>
236     <xsl:when test="m:prsubset">
237      <xsl:value-of select="'&#204;'"/>
238     </xsl:when>
239     <xsl:when test="m:setdiff">
240      <xsl:value-of select="'/'"/>
241     </xsl:when>
242    </xsl:choose>
243   </xsl:variable>
244   <xsl:choose>
245     <xsl:when test="$charlength > $framewidth">
246      <xsl:text>(</xsl:text>
247      <xsl:apply-templates select="*[2]">
248       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
249      </xsl:apply-templates>
250      <BR/> 
251      <xsl:call-template name="make_indent">
252       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
253      </xsl:call-template>
254      <a href="{$uri}">
255       <xsl:call-template name="mksymbol">
256        <xsl:with-param name="symbol">
257         <xsl:value-of select="local-name(*[1])"/>
258        </xsl:with-param>
259       </xsl:call-template>
260      </a>
261      <xsl:apply-templates select="*[3]">
262       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
263      </xsl:apply-templates>
264      <xsl:text>)</xsl:text>
265     </xsl:when>
266     <xsl:otherwise>
267      <xsl:apply-templates mode="inline" select="."/>
268     </xsl:otherwise>
269    </xsl:choose>
270  </xsl:template>
271
272
273 <!-- SET -->
274
275  <xsl:template match="m:set">
276   <xsl:param name="current_indent" select="0"/> 
277   <xsl:param name="width" select="$framewidth"/>
278   <xsl:variable name="uri" select="@definitionURL"/>
279 <!--   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
280   </xsl:variable>-->
281   <xsl:choose>
282    <xsl:when test="count(child::*) = 0">
283     <xsl:call-template name="mksymbol">
284      <xsl:with-param name="symbol" select="'emptyset'"/>
285     </xsl:call-template>
286    </xsl:when>
287    <xsl:otherwise>
288     <xsl:variable name="charlength">
289      <xsl:apply-templates select="." mode="charcount"/>
290     </xsl:variable>
291     <xsl:choose>
292      <xsl:when test="$charlength > $framewidth">
293       <xsl:choose>
294        <xsl:when test="name(*[1]) = 'm:bvar'">
295         <xsl:text>{</xsl:text>
296         <xsl:apply-templates select="m:bvar/m:ci"/>
297         <xsl:text>:</xsl:text>
298         <xsl:apply-templates select="m:bvar/m:type">
299          <xsl:with-param name="current_indent" 
300            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
301         </xsl:apply-templates><BR/>
302         <xsl:call-template name="make_indent">
303          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
304         </xsl:call-template>
305         <xsl:text>|</xsl:text>
306         <xsl:apply-templates select="m:condition">
307          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
308         </xsl:apply-templates>
309         <xsl:text>}</xsl:text>
310        </xsl:when>
311        <xsl:otherwise>
312         <xsl:text>{</xsl:text>
313          <xsl:apply-templates select="*[position()=1]">
314           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
315          </xsl:apply-templates>
316          <xsl:for-each select="*[position()>1]">
317           <xsl:text>,</xsl:text>
318           <BR/>
319           <xsl:call-template name="make_indent">
320            <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
321           </xsl:call-template>
322           <xsl:apply-templates select=".">
323            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
324           </xsl:apply-templates>
325          </xsl:for-each>
326         <xsl:text>}</xsl:text>
327        </xsl:otherwise>
328       </xsl:choose>
329      </xsl:when>
330      <xsl:otherwise>
331       <xsl:apply-templates mode="inline" select="."/>
332      </xsl:otherwise>
333     </xsl:choose>
334    </xsl:otherwise>
335   </xsl:choose>
336  </xsl:template> 
337
338 <!-- CARD -->
339 <xsl:template match="m:apply[m:card]">
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:card/@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 <!-- COUNTING -->
353
354 <xsl:template match="m:in|m:notin|m:intersect|m:union
355            |m:subset|m:prsubset|m:setdiff|m:card" mode="charcount">
356 <xsl:param name="incurrent_length" select="0"/> 
357     <xsl:choose>
358     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
359      <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>
360      <xsl:choose>
361      <xsl:when test="string($siblength) = &quot;&quot;">
362       <xsl:value-of select="$incurrent_length + string-length()"/>
363      </xsl:when>
364      <xsl:otherwise>
365       <xsl:value-of select="number($siblength)"/>
366      </xsl:otherwise>
367      </xsl:choose>
368     </xsl:when>
369     <xsl:otherwise>
370      <xsl:value-of select="$incurrent_length + string-length()"/>
371     </xsl:otherwise>
372     </xsl:choose>
373 </xsl:template> 
374
375 </xsl:stylesheet> 
376
377
378
379
380
381
382