2 <!-- Copyright (C) 2000, HELM Team -->
3 <!-- This file is part of HELM, an Hypertextual, Electronic -->
4 <!-- Library of Mathematics, developed at the Computer Science -->
5 <!-- Department, University of Bologna, Italy. -->
6 <!-- HELM is free software; you can redistribute it and/or -->
7 <!-- modify it under the terms of the GNU General Public License -->
8 <!-- as published by the Free Software Foundation; either version 2 -->
9 <!-- of the License, or (at your option) any later version. -->
10 <!-- HELM is distributed in the hope that it will be useful, -->
11 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
12 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
13 <!-- GNU General Public License for more details. -->
14 <!-- You should have received a copy of the GNU General Public License -->
15 <!-- along with HELM; if not, write to the Free Software -->
16 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
17 <!-- MA 02111-1307, USA. -->
18 <!-- For details, see the HELM World-Wide-Web page, -->
19 <!-- http://cs.unibo.it/helm/. -->
20 <xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:i="http://www.cs.unibo.it/helm/InputNotationalElements" xmlns:o="http://www.cs.unibo.it/helm/OutputNotationalElements" version="1.0">
23 <xsl:variable name="and">
25 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Ù</xsl:when>
26 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∧</xsl:when>
27 <xsl:otherwise>???</xsl:otherwise>
31 <xsl:variable name="or">
33 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Ú</xsl:when>
34 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∨</xsl:when>
35 <xsl:otherwise>???</xsl:otherwise>
39 <xsl:variable name="iff">
41 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Û</xsl:when>
42 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">⇔</xsl:when>
43 <xsl:otherwise>???</xsl:otherwise>
47 <xsl:variable name="not">
49 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Ø</xsl:when>
50 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">¬</xsl:when>
51 <xsl:otherwise>???</xsl:otherwise>
55 <xsl:variable name="eq">
57 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">=</xsl:when>
58 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">=</xsl:when>
59 <xsl:otherwise>???</xsl:otherwise>
63 <xsl:variable name="neq">
65 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">¹</xsl:when>
66 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">≠</xsl:when>
67 <xsl:otherwise>???</xsl:otherwise>
71 <xsl:variable name="exists">
73 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">$</xsl:when>
74 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∃</xsl:when>
75 <xsl:otherwise>???</xsl:otherwise>
79 <xsl:template match="m:apply[m:and[count(*) = 0] and count(*) = 3]">
80 <xsl:param name="current_indent" select="0"/>
81 <xsl:param name="width" select="$framewidth"/>
82 <xsl:variable name="charlength">
83 <xsl:apply-templates select="." mode="root_charcount"/>
86 <xsl:when test="$width >= $charlength">
87 <xsl:apply-templates select="." mode="inline"/>
90 <xsl:text>(</xsl:text>
91 <xsl:apply-templates select="*[2]">
92 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
93 </xsl:apply-templates>
95 <xsl:call-template name="make_indent">
96 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
98 <a href="{m:and/@definitionURL}">
100 <xsl:when test="boolean($and)">
101 <xsl:call-template name="mksymbol">
102 <xsl:with-param name="symbol" select="$and"/>
105 <xsl:otherwise>and</xsl:otherwise>
108 <xsl:apply-templates select="*[3]">
109 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
110 </xsl:apply-templates>
111 <xsl:text>)</xsl:text>
115 <!-- AND (INLINE MODE) -->
116 <xsl:template match="m:apply[m:and[count(*) = 0] and count(*) = 3]" mode="inline">
117 <xsl:text>(</xsl:text>
118 <xsl:apply-templates select="*[2]" mode="inline"/>
119 <a href="{m:and/@definitionURL}">
121 <xsl:when test="boolean($and)">
122 <xsl:call-template name="mksymbol">
123 <xsl:with-param name="symbol" select="$and"/>
126 <xsl:otherwise>and</xsl:otherwise>
129 <xsl:apply-templates select="*[3]" mode="inline"/>
130 <xsl:text>)</xsl:text>
132 <!-- AND (CHARCOUNT MODE) -->
133 <xsl:template match="m:apply[m:and[count(*) = 0] and count(*) = 3]" mode="root_charcount">
134 <xsl:param name="incurrent_length" select="0"/>
135 <xsl:value-of select="$incurrent_length + 3"/>
138 <xsl:template match="m:apply[m:or[count(*) = 0] and count(*) = 3]">
139 <xsl:param name="current_indent" select="0"/>
140 <xsl:param name="width" select="$framewidth"/>
141 <xsl:variable name="charlength">
142 <xsl:apply-templates select="." mode="root_charcount"/>
145 <xsl:when test="$width >= $charlength">
146 <xsl:apply-templates select="." mode="inline"/>
149 <xsl:text>(</xsl:text>
150 <xsl:apply-templates select="*[2]">
151 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
152 </xsl:apply-templates>
154 <xsl:call-template name="make_indent">
155 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
157 <a href="{m:or/@definitionURL}">
159 <xsl:when test="boolean($or)">
160 <xsl:call-template name="mksymbol">
161 <xsl:with-param name="symbol" select="$or"/>
164 <xsl:otherwise>or</xsl:otherwise>
167 <xsl:apply-templates select="*[3]">
168 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
169 </xsl:apply-templates>
170 <xsl:text>)</xsl:text>
174 <!-- OR (INLINE MODE) -->
175 <xsl:template match="m:apply[m:or[count(*) = 0] and count(*) = 3]" mode="inline">
176 <xsl:text>(</xsl:text>
177 <xsl:apply-templates select="*[2]" mode="inline"/>
178 <a href="{m:or/@definitionURL}">
180 <xsl:when test="boolean($or)">
181 <xsl:call-template name="mksymbol">
182 <xsl:with-param name="symbol" select="$or"/>
185 <xsl:otherwise>or</xsl:otherwise>
188 <xsl:apply-templates select="*[3]" mode="inline"/>
189 <xsl:text>)</xsl:text>
191 <!-- OR (CHARCOUNT MODE) -->
192 <xsl:template match="m:apply[m:or[count(*) = 0] and count(*) = 3]" mode="root_charcount">
193 <xsl:param name="incurrent_length" select="0"/>
194 <xsl:value-of select="$incurrent_length + 3"/>
197 <xsl:template match="m:apply[m:csymbol[text() = 'iff' and count(*) = 0] and count(*) = 3]">
198 <xsl:param name="current_indent" select="0"/>
199 <xsl:param name="width" select="$framewidth"/>
200 <xsl:variable name="charlength">
201 <xsl:apply-templates select="." mode="root_charcount"/>
204 <xsl:when test="$width >= $charlength">
205 <xsl:apply-templates select="." mode="inline"/>
208 <xsl:text>(</xsl:text>
209 <xsl:apply-templates select="*[2]">
210 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
211 </xsl:apply-templates>
213 <xsl:call-template name="make_indent">
214 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
216 <a href="{m:csymbol/@definitionURL}">
218 <xsl:when test="boolean($iff)">
219 <xsl:call-template name="mksymbol">
220 <xsl:with-param name="symbol" select="$iff"/>
223 <xsl:otherwise>iff</xsl:otherwise>
226 <xsl:apply-templates select="*[3]">
227 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
228 </xsl:apply-templates>
229 <xsl:text>)</xsl:text>
233 <!-- IFF (INLINE MODE) -->
234 <xsl:template match="m:apply[m:csymbol[text() = 'iff' and count(*) = 0] and count(*) = 3]" mode="inline">
235 <xsl:text>(</xsl:text>
236 <xsl:apply-templates select="*[2]" mode="inline"/>
237 <a href="{m:csymbol/@definitionURL}">
239 <xsl:when test="boolean($iff)">
240 <xsl:call-template name="mksymbol">
241 <xsl:with-param name="symbol" select="$iff"/>
244 <xsl:otherwise>iff</xsl:otherwise>
247 <xsl:apply-templates select="*[3]" mode="inline"/>
248 <xsl:text>)</xsl:text>
250 <!-- IFF (CHARCOUNT MODE) -->
251 <xsl:template match="m:apply[m:csymbol[text() = 'iff' and count(*) = 0] and count(*) = 3]" mode="root_charcount">
252 <xsl:param name="incurrent_length" select="0"/>
253 <xsl:value-of select="$incurrent_length + 3"/>
256 <xsl:template match="m:apply[m:not[count(*) = 0] and count(*) = 2]">
257 <xsl:param name="current_indent" select="0"/>
258 <xsl:param name="width" select="$framewidth"/>
259 <a href="{m:not/@definitionURL}">
261 <xsl:when test="boolean($not)">
262 <xsl:call-template name="mksymbol">
263 <xsl:with-param name="symbol" select="$not"/>
266 <xsl:otherwise>not</xsl:otherwise>
269 <xsl:apply-templates select="*[2]">
270 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
271 </xsl:apply-templates>
273 <!-- NOT (INLINE MODE) -->
274 <xsl:template match="m:apply[m:not[count(*) = 0] and count(*) = 2]" mode="inline">
275 <a href="{m:not/@definitionURL}">
277 <xsl:when test="boolean($not)">
278 <xsl:call-template name="mksymbol">
279 <xsl:with-param name="symbol" select="$not"/>
282 <xsl:otherwise>not</xsl:otherwise>
285 <xsl:apply-templates select="*[2]" mode="inline"/>
287 <!-- NOT (CHARCOUNT MODE) -->
288 <xsl:template match="m:apply[m:not[count(*) = 0] and count(*) = 2]" mode="root_charcount">
289 <xsl:param name="incurrent_length" select="0"/>
290 <xsl:value-of select="$incurrent_length + 1"/>
292 <!-- EQUALITY and TYPE EQUALITY -->
293 <xsl:template match="m:apply[m:eq[count(*) = 0] and count(*) = 3]">
294 <xsl:param name="current_indent" select="0"/>
295 <xsl:param name="width" select="$framewidth"/>
296 <xsl:variable name="charlength">
297 <xsl:apply-templates select="." mode="root_charcount"/>
300 <xsl:when test="$width >= $charlength">
301 <xsl:apply-templates select="." mode="inline"/>
304 <xsl:text>(</xsl:text>
305 <xsl:apply-templates select="*[2]">
306 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
307 </xsl:apply-templates>
309 <xsl:call-template name="make_indent">
310 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
312 <a href="{m:eq/@definitionURL}">
314 <xsl:when test="boolean($eq)">
315 <xsl:call-template name="mksymbol">
316 <xsl:with-param name="symbol" select="$eq"/>
319 <xsl:otherwise>eq</xsl:otherwise>
322 <xsl:apply-templates select="*[3]">
323 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
324 </xsl:apply-templates>
325 <xsl:text>)</xsl:text>
329 <!-- EQUALITY and TYPE EQUALITY (INLINE MODE) -->
330 <xsl:template match="m:apply[m:eq[count(*) = 0] and count(*) = 3]" mode="inline">
331 <xsl:text>(</xsl:text>
332 <xsl:apply-templates select="*[2]" mode="inline"/>
333 <a href="{m:eq/@definitionURL}">
335 <xsl:when test="boolean($eq)">
336 <xsl:call-template name="mksymbol">
337 <xsl:with-param name="symbol" select="$eq"/>
340 <xsl:otherwise>eq</xsl:otherwise>
343 <xsl:apply-templates select="*[3]" mode="inline"/>
344 <xsl:text>)</xsl:text>
346 <!-- EQUALITY and TYPE EQUALITY (CHARCOUNT MODE) -->
347 <xsl:template match="m:apply[m:eq[count(*) = 0] and count(*) = 3]" mode="root_charcount">
348 <xsl:param name="incurrent_length" select="0"/>
349 <xsl:value-of select="$incurrent_length + 3"/>
351 <!-- NOT-EQ and NOT-EQT -->
352 <xsl:template match="m:apply[m:neq[count(*) = 0] and count(*) = 3]">
353 <xsl:param name="current_indent" select="0"/>
354 <xsl:param name="width" select="$framewidth"/>
355 <xsl:variable name="charlength">
356 <xsl:apply-templates select="." mode="root_charcount"/>
359 <xsl:when test="$width >= $charlength">
360 <xsl:apply-templates select="." mode="inline"/>
363 <xsl:text>(</xsl:text>
364 <xsl:apply-templates select="*[2]">
365 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
366 </xsl:apply-templates>
368 <xsl:call-template name="make_indent">
369 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
371 <a href="{m:neq/@definitionURL}">
373 <xsl:when test="boolean($neq)">
374 <xsl:call-template name="mksymbol">
375 <xsl:with-param name="symbol" select="$neq"/>
378 <xsl:otherwise>neq</xsl:otherwise>
381 <xsl:apply-templates select="*[3]">
382 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
383 </xsl:apply-templates>
384 <xsl:text>)</xsl:text>
388 <!-- NOT-EQ and NOT-EQT (INLINE MODE) -->
389 <xsl:template match="m:apply[m:neq[count(*) = 0] and count(*) = 3]" mode="inline">
390 <xsl:text>(</xsl:text>
391 <xsl:apply-templates select="*[2]" mode="inline"/>
392 <a href="{m:neq/@definitionURL}">
394 <xsl:when test="boolean($neq)">
395 <xsl:call-template name="mksymbol">
396 <xsl:with-param name="symbol" select="$neq"/>
399 <xsl:otherwise>neq</xsl:otherwise>
402 <xsl:apply-templates select="*[3]" mode="inline"/>
403 <xsl:text>)</xsl:text>
405 <!-- NOT-EQ and NOT-EQT (CHARCOUNT MODE) -->
406 <xsl:template match="m:apply[m:neq[count(*) = 0] and count(*) = 3]" mode="root_charcount">
407 <xsl:param name="incurrent_length" select="0"/>
408 <xsl:value-of select="$incurrent_length + 3"/>
411 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]">
412 <xsl:param name="current_indent" select="0"/>
413 <xsl:param name="width" select="$framewidth"/>
414 <xsl:variable name="charlength">
415 <xsl:apply-templates select="." mode="root_charcount"/>
418 <xsl:when test="$width >= $charlength">
419 <xsl:apply-templates select="." mode="inline"/>
422 <a href="{m:exists/@definitionURL}">
424 <xsl:when test="boolean($exists)">
425 <xsl:call-template name="mksymbol">
426 <xsl:with-param name="symbol" select="$exists"/>
429 <xsl:otherwise>exists</xsl:otherwise>
432 <xsl:value-of select="m:bvar/m:ci/text()"/>
433 <xsl:text>:</xsl:text>
434 <xsl:apply-templates select="m:condition/*[1]">
435 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
436 </xsl:apply-templates>
438 <xsl:call-template name="make_indent">
439 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
441 <xsl:text>.</xsl:text>
442 <xsl:apply-templates select="*[4]">
443 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
444 </xsl:apply-templates>
448 <!-- EXIST (INLINE MODE) -->
449 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]" mode="inline">
450 <a href="{m:exists/@definitionURL}">
452 <xsl:when test="boolean($exists)">
453 <xsl:call-template name="mksymbol">
454 <xsl:with-param name="symbol" select="$exists"/>
457 <xsl:otherwise>exists</xsl:otherwise>
460 <xsl:value-of select="m:bvar/m:ci/text()"/>
461 <xsl:text>:</xsl:text>
462 <xsl:apply-templates select="m:condition/*[1]" mode="inline"/>
463 <xsl:text>.</xsl:text>
464 <xsl:apply-templates select="*[4]" mode="inline"/>
466 <!-- EXIST (CHARCOUNT MODE) -->
467 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]" mode="root_charcount">
468 <xsl:param name="incurrent_length" select="0"/>
469 <xsl:value-of select="$incurrent_length + 3"/>
472 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]">
473 <xsl:param name="current_indent" select="0"/>
474 <xsl:param name="width" select="$framewidth"/>
475 <xsl:variable name="charlength">
476 <xsl:apply-templates select="." mode="root_charcount"/>
479 <xsl:when test="$width >= $charlength">
480 <xsl:apply-templates select="." mode="inline"/>
483 <a href="{m:exists/@definitionURL}">
485 <xsl:when test="boolean($exists)">
486 <xsl:call-template name="mksymbol">
487 <xsl:with-param name="symbol" select="$exists"/>
490 <xsl:otherwise>exists</xsl:otherwise>
493 <xsl:value-of select="m:bvar/m:ci/text()"/>
494 <xsl:text>:</xsl:text>
495 <xsl:apply-templates select="m:condition/*[1]">
496 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
497 </xsl:apply-templates>
499 <xsl:call-template name="make_indent">
500 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
502 <xsl:text>.</xsl:text>
503 <xsl:apply-templates select="*[4]">
504 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
505 </xsl:apply-templates>
509 <!-- EXIST (INLINE MODE) -->
510 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]" mode="inline">
511 <a href="{m:exists/@definitionURL}">
513 <xsl:when test="boolean($exists)">
514 <xsl:call-template name="mksymbol">
515 <xsl:with-param name="symbol" select="$exists"/>
518 <xsl:otherwise>exists</xsl:otherwise>
521 <xsl:value-of select="m:bvar/m:ci/text()"/>
522 <xsl:text>:</xsl:text>
523 <xsl:apply-templates select="m:condition/*[1]" mode="inline"/>
524 <xsl:text>.</xsl:text>
525 <xsl:apply-templates select="*[4]" mode="inline"/>
527 <!-- EXIST (CHARCOUNT MODE) -->
528 <xsl:template match="m:apply[m:exists[count(*) = 0] and m:bvar/m:ci[count(*) = 0] and m:condition[count(*) = 1] and count(*) = 4]" mode="root_charcount">
529 <xsl:param name="incurrent_length" select="0"/>
530 <xsl:value-of select="$incurrent_length + 3"/>