]> matita.cs.unibo.it Git - helm.git/blob - helm/nuprl_stylesheets/nuprl_html_arith.xsl
incomplete proof completed
[helm.git] / helm / nuprl_stylesheets / nuprl_html_arith.xsl
1 <?xml version="1.0"?>
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">
21 <!-- HTML SYMBOLS  -->
22 <!--leq-->
23   <xsl:variable name="leq">
24     <xsl:choose>
25       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xA3;</xsl:when>
26       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2264;</xsl:when>
27       <xsl:otherwise>???</xsl:otherwise>
28     </xsl:choose>
29   </xsl:variable>
30 <!--lt-->
31   <xsl:variable name="lt">
32     <xsl:choose>
33       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&lt;</xsl:when>
34       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&lt; </xsl:when>
35       <xsl:otherwise>???</xsl:otherwise>
36     </xsl:choose>
37   </xsl:variable>
38 <!--geq-->
39   <xsl:variable name="geq">
40     <xsl:choose>
41       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xB3;</xsl:when>
42       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2265;</xsl:when>
43       <xsl:otherwise>???</xsl:otherwise>
44     </xsl:choose>
45   </xsl:variable>
46 <!--gt-->
47   <xsl:variable name="gt">
48     <xsl:choose>
49       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&gt;</xsl:when>
50       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&gt;</xsl:when>
51       <xsl:otherwise>???</xsl:otherwise>
52     </xsl:choose>
53   </xsl:variable>
54 <!--plus-->
55   <xsl:variable name="plus">
56     <xsl:choose>
57       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">+</xsl:when>
58       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">+</xsl:when>
59       <xsl:otherwise>???</xsl:otherwise>
60     </xsl:choose>
61   </xsl:variable>
62 <!--minus-->
63   <xsl:variable name="minus">
64     <xsl:choose>
65       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">-</xsl:when>
66       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">-</xsl:when>
67       <xsl:otherwise>???</xsl:otherwise>
68     </xsl:choose>
69   </xsl:variable>
70 <!--times-->
71   <xsl:variable name="times">
72     <xsl:choose>
73       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">*</xsl:when>
74       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2217;</xsl:when>
75       <xsl:otherwise>???</xsl:otherwise>
76     </xsl:choose>
77   </xsl:variable>
78 <!--min-->
79   <xsl:variable name="min" select="'min'"/>
80 <!--abs-->
81   <xsl:variable name="abs" select="'|'"/>
82 <!-- LESS EQUAL -->
83   <xsl:template match="m:apply[m:leq[count(*) = 0] and count(*) = 3]">
84     <xsl:param name="current_indent" select="0"/>
85     <xsl:param name="width" select="$framewidth"/>
86     <xsl:variable name="charlength">
87       <xsl:apply-templates select="." mode="root_charcount"/>
88     </xsl:variable>
89     <xsl:choose>
90       <xsl:when test="$width &gt;= $charlength">
91         <xsl:apply-templates select="." mode="inline"/>
92       </xsl:when>
93       <xsl:otherwise>
94         <xsl:text>(</xsl:text>
95         <xsl:apply-templates select="*[2]">
96           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
97         </xsl:apply-templates>
98         <BR/>
99         <xsl:call-template name="make_indent">
100           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
101         </xsl:call-template>
102         <a href="{m:leq/@definitionURL}">
103           <xsl:choose>
104             <xsl:when test="boolean($leq)">
105               <xsl:call-template name="mksymbol">
106                 <xsl:with-param name="symbol" select="$leq"/>
107               </xsl:call-template>
108             </xsl:when>
109             <xsl:otherwise>leq</xsl:otherwise>
110           </xsl:choose>
111         </a>
112         <xsl:apply-templates select="*[3]">
113           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
114         </xsl:apply-templates>
115         <xsl:text>)</xsl:text>
116       </xsl:otherwise>
117     </xsl:choose>
118   </xsl:template>
119 <!-- LESS EQUAL (INLINE MODE) -->
120   <xsl:template match="m:apply[m:leq[count(*) = 0] and count(*) = 3]" mode="inline">
121     <xsl:text>(</xsl:text>
122     <xsl:apply-templates select="*[2]" mode="inline"/>
123     <a href="{m:leq/@definitionURL}">
124       <xsl:choose>
125         <xsl:when test="boolean($leq)">
126           <xsl:call-template name="mksymbol">
127             <xsl:with-param name="symbol" select="$leq"/>
128           </xsl:call-template>
129         </xsl:when>
130         <xsl:otherwise>leq</xsl:otherwise>
131       </xsl:choose>
132     </a>
133     <xsl:apply-templates select="*[3]" mode="inline"/>
134     <xsl:text>)</xsl:text>
135   </xsl:template>
136 <!-- LESS EQUAL (CHARCOUNT MODE) -->
137   <xsl:template match="m:apply[m:leq[count(*) = 0] and count(*) = 3]" mode="root_charcount">
138     <xsl:param name="incurrent_length" select="0"/>
139     <xsl:value-of select="$incurrent_length + 3"/>
140   </xsl:template>
141 <!-- LESS THAN -->
142   <xsl:template match="m:apply[m:lt[count(*) = 0] and count(*) = 3]">
143     <xsl:param name="current_indent" select="0"/>
144     <xsl:param name="width" select="$framewidth"/>
145     <xsl:variable name="charlength">
146       <xsl:apply-templates select="." mode="root_charcount"/>
147     </xsl:variable>
148     <xsl:choose>
149       <xsl:when test="$width &gt;= $charlength">
150         <xsl:apply-templates select="." mode="inline"/>
151       </xsl:when>
152       <xsl:otherwise>
153         <xsl:text>(</xsl:text>
154         <xsl:apply-templates select="*[2]">
155           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
156         </xsl:apply-templates>
157         <BR/>
158         <xsl:call-template name="make_indent">
159           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
160         </xsl:call-template>
161         <a href="{m:lt/@definitionURL}">
162           <xsl:choose>
163             <xsl:when test="boolean($lt)">
164               <xsl:call-template name="mksymbol">
165                 <xsl:with-param name="symbol" select="$lt"/>
166               </xsl:call-template>
167             </xsl:when>
168             <xsl:otherwise>lt</xsl:otherwise>
169           </xsl:choose>
170         </a>
171         <xsl:apply-templates select="*[3]">
172           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
173         </xsl:apply-templates>
174         <xsl:text>)</xsl:text>
175       </xsl:otherwise>
176     </xsl:choose>
177   </xsl:template>
178 <!-- LESS THAN (INLINE MODE) -->
179   <xsl:template match="m:apply[m:lt[count(*) = 0] and count(*) = 3]" mode="inline">
180     <xsl:text>(</xsl:text>
181     <xsl:apply-templates select="*[2]" mode="inline"/>
182     <a href="{m:lt/@definitionURL}">
183       <xsl:choose>
184         <xsl:when test="boolean($lt)">
185           <xsl:call-template name="mksymbol">
186             <xsl:with-param name="symbol" select="$lt"/>
187           </xsl:call-template>
188         </xsl:when>
189         <xsl:otherwise>lt</xsl:otherwise>
190       </xsl:choose>
191     </a>
192     <xsl:apply-templates select="*[3]" mode="inline"/>
193     <xsl:text>)</xsl:text>
194   </xsl:template>
195 <!-- LESS THAN (CHARCOUNT MODE) -->
196   <xsl:template match="m:apply[m:lt[count(*) = 0] and count(*) = 3]" mode="root_charcount">
197     <xsl:param name="incurrent_length" select="0"/>
198     <xsl:value-of select="$incurrent_length + 3"/>
199   </xsl:template>
200 <!-- GREATER EQUAL -->
201   <xsl:template match="m:apply[m:geq[count(*) = 0] and count(*) = 3]">
202     <xsl:param name="current_indent" select="0"/>
203     <xsl:param name="width" select="$framewidth"/>
204     <xsl:variable name="charlength">
205       <xsl:apply-templates select="." mode="root_charcount"/>
206     </xsl:variable>
207     <xsl:choose>
208       <xsl:when test="$width &gt;= $charlength">
209         <xsl:apply-templates select="." mode="inline"/>
210       </xsl:when>
211       <xsl:otherwise>
212         <xsl:text>(</xsl:text>
213         <xsl:apply-templates select="*[2]">
214           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
215         </xsl:apply-templates>
216         <BR/>
217         <xsl:call-template name="make_indent">
218           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
219         </xsl:call-template>
220         <a href="{m:geq/@definitionURL}">
221           <xsl:choose>
222             <xsl:when test="boolean($geq)">
223               <xsl:call-template name="mksymbol">
224                 <xsl:with-param name="symbol" select="$geq"/>
225               </xsl:call-template>
226             </xsl:when>
227             <xsl:otherwise>geq</xsl:otherwise>
228           </xsl:choose>
229         </a>
230         <xsl:apply-templates select="*[3]">
231           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
232         </xsl:apply-templates>
233         <xsl:text>)</xsl:text>
234       </xsl:otherwise>
235     </xsl:choose>
236   </xsl:template>
237 <!-- GREATER EQUAL (INLINE MODE) -->
238   <xsl:template match="m:apply[m:geq[count(*) = 0] and count(*) = 3]" mode="inline">
239     <xsl:text>(</xsl:text>
240     <xsl:apply-templates select="*[2]" mode="inline"/>
241     <a href="{m:geq/@definitionURL}">
242       <xsl:choose>
243         <xsl:when test="boolean($geq)">
244           <xsl:call-template name="mksymbol">
245             <xsl:with-param name="symbol" select="$geq"/>
246           </xsl:call-template>
247         </xsl:when>
248         <xsl:otherwise>geq</xsl:otherwise>
249       </xsl:choose>
250     </a>
251     <xsl:apply-templates select="*[3]" mode="inline"/>
252     <xsl:text>)</xsl:text>
253   </xsl:template>
254 <!-- GREATER EQUAL (CHARCOUNT MODE) -->
255   <xsl:template match="m:apply[m:geq[count(*) = 0] and count(*) = 3]" mode="root_charcount">
256     <xsl:param name="incurrent_length" select="0"/>
257     <xsl:value-of select="$incurrent_length + 3"/>
258   </xsl:template>
259 <!-- GREATER THAN -->
260   <xsl:template match="m:apply[m:gt[count(*) = 0] and count(*) = 3]">
261     <xsl:param name="current_indent" select="0"/>
262     <xsl:param name="width" select="$framewidth"/>
263     <xsl:variable name="charlength">
264       <xsl:apply-templates select="." mode="root_charcount"/>
265     </xsl:variable>
266     <xsl:choose>
267       <xsl:when test="$width &gt;= $charlength">
268         <xsl:apply-templates select="." mode="inline"/>
269       </xsl:when>
270       <xsl:otherwise>
271         <xsl:text>(</xsl:text>
272         <xsl:apply-templates select="*[2]">
273           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
274         </xsl:apply-templates>
275         <BR/>
276         <xsl:call-template name="make_indent">
277           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
278         </xsl:call-template>
279         <a href="{m:gt/@definitionURL}">
280           <xsl:choose>
281             <xsl:when test="boolean($gt)">
282               <xsl:call-template name="mksymbol">
283                 <xsl:with-param name="symbol" select="$gt"/>
284               </xsl:call-template>
285             </xsl:when>
286             <xsl:otherwise>gt</xsl:otherwise>
287           </xsl:choose>
288         </a>
289         <xsl:apply-templates select="*[3]">
290           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
291         </xsl:apply-templates>
292         <xsl:text>)</xsl:text>
293       </xsl:otherwise>
294     </xsl:choose>
295   </xsl:template>
296 <!-- GREATER THAN (INLINE MODE) -->
297   <xsl:template match="m:apply[m:gt[count(*) = 0] and count(*) = 3]" mode="inline">
298     <xsl:text>(</xsl:text>
299     <xsl:apply-templates select="*[2]" mode="inline"/>
300     <a href="{m:gt/@definitionURL}">
301       <xsl:choose>
302         <xsl:when test="boolean($gt)">
303           <xsl:call-template name="mksymbol">
304             <xsl:with-param name="symbol" select="$gt"/>
305           </xsl:call-template>
306         </xsl:when>
307         <xsl:otherwise>gt</xsl:otherwise>
308       </xsl:choose>
309     </a>
310     <xsl:apply-templates select="*[3]" mode="inline"/>
311     <xsl:text>)</xsl:text>
312   </xsl:template>
313 <!-- GREATER THAN (CHARCOUNT MODE) -->
314   <xsl:template match="m:apply[m:gt[count(*) = 0] and count(*) = 3]" mode="root_charcount">
315     <xsl:param name="incurrent_length" select="0"/>
316     <xsl:value-of select="$incurrent_length + 3"/>
317   </xsl:template>
318 <!-- PLUS -->
319   <xsl:template match="m:apply[m:plus[count(*) = 0] and count(*) = 3]">
320     <xsl:param name="current_indent" select="0"/>
321     <xsl:param name="width" select="$framewidth"/>
322     <xsl:variable name="charlength">
323       <xsl:apply-templates select="." mode="root_charcount"/>
324     </xsl:variable>
325     <xsl:choose>
326       <xsl:when test="$width &gt;= $charlength">
327         <xsl:apply-templates select="." mode="inline"/>
328       </xsl:when>
329       <xsl:otherwise>
330         <xsl:text>(</xsl:text>
331         <xsl:apply-templates select="*[2]">
332           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
333         </xsl:apply-templates>
334         <BR/>
335         <xsl:call-template name="make_indent">
336           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
337         </xsl:call-template>
338         <a href="{m:plus/@definitionURL}">
339           <xsl:choose>
340             <xsl:when test="boolean($plus)">
341               <xsl:call-template name="mksymbol">
342                 <xsl:with-param name="symbol" select="$plus"/>
343               </xsl:call-template>
344             </xsl:when>
345             <xsl:otherwise>plus</xsl:otherwise>
346           </xsl:choose>
347         </a>
348         <xsl:apply-templates select="*[3]">
349           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
350         </xsl:apply-templates>
351         <xsl:text>)</xsl:text>
352       </xsl:otherwise>
353     </xsl:choose>
354   </xsl:template>
355 <!-- PLUS (INLINE MODE) -->
356   <xsl:template match="m:apply[m:plus[count(*) = 0] and count(*) = 3]" mode="inline">
357     <xsl:text>(</xsl:text>
358     <xsl:apply-templates select="*[2]" mode="inline"/>
359     <a href="{m:plus/@definitionURL}">
360       <xsl:choose>
361         <xsl:when test="boolean($plus)">
362           <xsl:call-template name="mksymbol">
363             <xsl:with-param name="symbol" select="$plus"/>
364           </xsl:call-template>
365         </xsl:when>
366         <xsl:otherwise>plus</xsl:otherwise>
367       </xsl:choose>
368     </a>
369     <xsl:apply-templates select="*[3]" mode="inline"/>
370     <xsl:text>)</xsl:text>
371   </xsl:template>
372 <!-- PLUS (CHARCOUNT MODE) -->
373   <xsl:template match="m:apply[m:plus[count(*) = 0] and count(*) = 3]" mode="root_charcount">
374     <xsl:param name="incurrent_length" select="0"/>
375     <xsl:value-of select="$incurrent_length + 3"/>
376   </xsl:template>
377 <!-- MINUS -->
378   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 3]">
379     <xsl:param name="current_indent" select="0"/>
380     <xsl:param name="width" select="$framewidth"/>
381     <xsl:variable name="charlength">
382       <xsl:apply-templates select="." mode="root_charcount"/>
383     </xsl:variable>
384     <xsl:choose>
385       <xsl:when test="$width &gt;= $charlength">
386         <xsl:apply-templates select="." mode="inline"/>
387       </xsl:when>
388       <xsl:otherwise>
389         <xsl:text>(</xsl:text>
390         <xsl:apply-templates select="*[2]">
391           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
392         </xsl:apply-templates>
393         <BR/>
394         <xsl:call-template name="make_indent">
395           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
396         </xsl:call-template>
397         <a href="{m:minus/@definitionURL}">
398           <xsl:choose>
399             <xsl:when test="boolean($minus)">
400               <xsl:call-template name="mksymbol">
401                 <xsl:with-param name="symbol" select="$minus"/>
402               </xsl:call-template>
403             </xsl:when>
404             <xsl:otherwise>minus</xsl:otherwise>
405           </xsl:choose>
406         </a>
407         <xsl:apply-templates select="*[3]">
408           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
409         </xsl:apply-templates>
410         <xsl:text>)</xsl:text>
411       </xsl:otherwise>
412     </xsl:choose>
413   </xsl:template>
414 <!-- MINUS (INLINE MODE) -->
415   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 3]" mode="inline">
416     <xsl:text>(</xsl:text>
417     <xsl:apply-templates select="*[2]" mode="inline"/>
418     <a href="{m:minus/@definitionURL}">
419       <xsl:choose>
420         <xsl:when test="boolean($minus)">
421           <xsl:call-template name="mksymbol">
422             <xsl:with-param name="symbol" select="$minus"/>
423           </xsl:call-template>
424         </xsl:when>
425         <xsl:otherwise>minus</xsl:otherwise>
426       </xsl:choose>
427     </a>
428     <xsl:apply-templates select="*[3]" mode="inline"/>
429     <xsl:text>)</xsl:text>
430   </xsl:template>
431 <!-- MINUS (CHARCOUNT MODE) -->
432   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 3]" mode="root_charcount">
433     <xsl:param name="incurrent_length" select="0"/>
434     <xsl:value-of select="$incurrent_length + 3"/>
435   </xsl:template>
436 <!-- TIMES -->
437   <xsl:template match="m:apply[m:times[count(*) = 0] and count(*) = 3]">
438     <xsl:param name="current_indent" select="0"/>
439     <xsl:param name="width" select="$framewidth"/>
440     <xsl:variable name="charlength">
441       <xsl:apply-templates select="." mode="root_charcount"/>
442     </xsl:variable>
443     <xsl:choose>
444       <xsl:when test="$width &gt;= $charlength">
445         <xsl:apply-templates select="." mode="inline"/>
446       </xsl:when>
447       <xsl:otherwise>
448         <xsl:text>(</xsl:text>
449         <xsl:apply-templates select="*[2]">
450           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
451         </xsl:apply-templates>
452         <BR/>
453         <xsl:call-template name="make_indent">
454           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
455         </xsl:call-template>
456         <a href="{m:times/@definitionURL}">
457           <xsl:choose>
458             <xsl:when test="boolean($times)">
459               <xsl:call-template name="mksymbol">
460                 <xsl:with-param name="symbol" select="$times"/>
461               </xsl:call-template>
462             </xsl:when>
463             <xsl:otherwise>times</xsl:otherwise>
464           </xsl:choose>
465         </a>
466         <xsl:apply-templates select="*[3]">
467           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
468         </xsl:apply-templates>
469         <xsl:text>)</xsl:text>
470       </xsl:otherwise>
471     </xsl:choose>
472   </xsl:template>
473 <!-- TIMES (INLINE MODE) -->
474   <xsl:template match="m:apply[m:times[count(*) = 0] and count(*) = 3]" mode="inline">
475     <xsl:text>(</xsl:text>
476     <xsl:apply-templates select="*[2]" mode="inline"/>
477     <a href="{m:times/@definitionURL}">
478       <xsl:choose>
479         <xsl:when test="boolean($times)">
480           <xsl:call-template name="mksymbol">
481             <xsl:with-param name="symbol" select="$times"/>
482           </xsl:call-template>
483         </xsl:when>
484         <xsl:otherwise>times</xsl:otherwise>
485       </xsl:choose>
486     </a>
487     <xsl:apply-templates select="*[3]" mode="inline"/>
488     <xsl:text>)</xsl:text>
489   </xsl:template>
490 <!-- TIMES (CHARCOUNT MODE) -->
491   <xsl:template match="m:apply[m:times[count(*) = 0] and count(*) = 3]" mode="root_charcount">
492     <xsl:param name="incurrent_length" select="0"/>
493     <xsl:value-of select="$incurrent_length + 3"/>
494   </xsl:template>
495 <!-- MIN -->
496   <xsl:template match="m:apply[m:min[count(*) = 0] and count(*) = 3]">
497     <xsl:param name="current_indent" select="0"/>
498     <xsl:param name="width" select="$framewidth"/>
499     <xsl:variable name="charlength">
500       <xsl:apply-templates select="." mode="root_charcount"/>
501     </xsl:variable>
502     <xsl:choose>
503       <xsl:when test="$width &gt;= $charlength">
504         <xsl:apply-templates select="." mode="inline"/>
505       </xsl:when>
506       <xsl:otherwise>
507         <a href="{m:min/@definitionURL}">
508           <xsl:choose>
509             <xsl:when test="boolean($min)">
510               <xsl:call-template name="mksymbol">
511                 <xsl:with-param name="symbol" select="$min"/>
512               </xsl:call-template>
513             </xsl:when>
514             <xsl:otherwise>min</xsl:otherwise>
515           </xsl:choose>
516         </a>
517         <xsl:text>{</xsl:text>
518         <xsl:apply-templates select="*[2]">
519           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
520         </xsl:apply-templates>
521         <xsl:text>,</xsl:text>
522         <BR/>
523         <xsl:call-template name="make_indent">
524           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
525         </xsl:call-template>
526         <xsl:apply-templates select="*[3]">
527           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
528         </xsl:apply-templates>
529         <xsl:text>}</xsl:text>
530       </xsl:otherwise>
531     </xsl:choose>
532   </xsl:template>
533 <!-- MIN (INLINE MODE) -->
534   <xsl:template match="m:apply[m:min[count(*) = 0] and count(*) = 3]" mode="inline">
535     <a href="{m:min/@definitionURL}">
536       <xsl:choose>
537         <xsl:when test="boolean($min)">
538           <xsl:call-template name="mksymbol">
539             <xsl:with-param name="symbol" select="$min"/>
540           </xsl:call-template>
541         </xsl:when>
542         <xsl:otherwise>min</xsl:otherwise>
543       </xsl:choose>
544     </a>
545     <xsl:text>{</xsl:text>
546     <xsl:apply-templates select="*[2]" mode="inline"/>
547     <xsl:text>,</xsl:text>
548     <xsl:apply-templates select="*[3]" mode="inline"/>
549     <xsl:text>}</xsl:text>
550   </xsl:template>
551 <!-- MIN (CHARCOUNT MODE) -->
552   <xsl:template match="m:apply[m:min[count(*) = 0] and count(*) = 3]" mode="root_charcount">
553     <xsl:param name="incurrent_length" select="0"/>
554     <xsl:value-of select="$incurrent_length + 4"/>
555   </xsl:template>
556 <!-- MINUS -->
557   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 2]">
558     <xsl:param name="current_indent" select="0"/>
559     <xsl:param name="width" select="$framewidth"/>
560     <a href="{m:minus/@definitionURL}">
561       <xsl:choose>
562         <xsl:when test="boolean($minus)">
563           <xsl:call-template name="mksymbol">
564             <xsl:with-param name="symbol" select="$minus"/>
565           </xsl:call-template>
566         </xsl:when>
567         <xsl:otherwise>minus</xsl:otherwise>
568       </xsl:choose>
569     </a>
570     <xsl:apply-templates select="*[2]">
571       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
572     </xsl:apply-templates>
573   </xsl:template>
574 <!-- MINUS (INLINE MODE) -->
575   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 2]" mode="inline">
576     <a href="{m:minus/@definitionURL}">
577       <xsl:choose>
578         <xsl:when test="boolean($minus)">
579           <xsl:call-template name="mksymbol">
580             <xsl:with-param name="symbol" select="$minus"/>
581           </xsl:call-template>
582         </xsl:when>
583         <xsl:otherwise>minus</xsl:otherwise>
584       </xsl:choose>
585     </a>
586     <xsl:apply-templates select="*[2]" mode="inline"/>
587   </xsl:template>
588 <!-- MINUS (CHARCOUNT MODE) -->
589   <xsl:template match="m:apply[m:minus[count(*) = 0] and count(*) = 2]" mode="root_charcount">
590     <xsl:param name="incurrent_length" select="0"/>
591     <xsl:value-of select="$incurrent_length + 1"/>
592   </xsl:template>
593 <!-- ABSOLUTE VALUE -->
594   <xsl:template match="m:apply[m:abs[count(*) = 0] and count(*) = 2]">
595     <xsl:param name="current_indent" select="0"/>
596     <xsl:param name="width" select="$framewidth"/>
597     <a href="{m:abs/@definitionURL}">
598       <xsl:choose>
599         <xsl:when test="boolean($abs)">
600           <xsl:call-template name="mksymbol">
601             <xsl:with-param name="symbol" select="$abs"/>
602           </xsl:call-template>
603         </xsl:when>
604         <xsl:otherwise>abs</xsl:otherwise>
605       </xsl:choose>
606     </a>
607     <xsl:apply-templates select="*[2]">
608       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
609     </xsl:apply-templates>
610     <a href="{m:abs/@definitionURL}">
611       <xsl:choose>
612         <xsl:when test="boolean($abs)">
613           <xsl:call-template name="mksymbol">
614             <xsl:with-param name="symbol" select="$abs"/>
615           </xsl:call-template>
616         </xsl:when>
617         <xsl:otherwise>abs</xsl:otherwise>
618       </xsl:choose>
619     </a>
620   </xsl:template>
621 <!-- ABSOLUTE VALUE (INLINE MODE) -->
622   <xsl:template match="m:apply[m:abs[count(*) = 0] and count(*) = 2]" mode="inline">
623     <a href="{m:abs/@definitionURL}">
624       <xsl:choose>
625         <xsl:when test="boolean($abs)">
626           <xsl:call-template name="mksymbol">
627             <xsl:with-param name="symbol" select="$abs"/>
628           </xsl:call-template>
629         </xsl:when>
630         <xsl:otherwise>abs</xsl:otherwise>
631       </xsl:choose>
632     </a>
633     <xsl:apply-templates select="*[2]" mode="inline"/>
634     <a href="{m:abs/@definitionURL}">
635       <xsl:choose>
636         <xsl:when test="boolean($abs)">
637           <xsl:call-template name="mksymbol">
638             <xsl:with-param name="symbol" select="$abs"/>
639           </xsl:call-template>
640         </xsl:when>
641         <xsl:otherwise>abs</xsl:otherwise>
642       </xsl:choose>
643     </a>
644   </xsl:template>
645 <!-- ABSOLUTE VALUE (CHARCOUNT MODE) -->
646   <xsl:template match="m:apply[m:abs[count(*) = 0] and count(*) = 2]" mode="root_charcount">
647     <xsl:param name="incurrent_length" select="0"/>
648     <xsl:value-of select="$incurrent_length + 2"/>
649   </xsl:template>
650 </xsl:stylesheet>