helm/style/content_to_html.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 <!-- From MathML content to HTML                                           -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi               -->
  33 <!--***********************************************************************-->
  34
  35 <xsl:param name="CICURI" select="''"/>
  36 <xsl:param name="type" select="'standalone'"/>
  37 <xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
  38
  39 <xsl:include href="html_init.xsl"/>
  40 <xsl:include href="html_set.xsl"/>
  41 <xsl:include href="html_reals.xsl"/>
  42
  43 <xsl:variable name="showcast" select="0"/>
  44
  45 <!--***********************************************************************-->
  46 <!-- HTML Head and Body                                                    -->
  47 <!--***********************************************************************-->
  48
  49 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
  50
  51 <!-- document needs method="xml" and searches locally for the dtd if        -->
  52 <!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
  53 <!-- For having output html must be media-type="html" and for having the    -->
  54 <!-- correct <br /> you must specify at least the remote dtd by means of    -->
  55 <!-- doctype-public                                                         -->
  56 <xsl:output
  57         method="xml"
  58         encoding="iso-8859-1"
  59         media-type="text/html"
  60         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  61
  62 <xsl:variable name="framewidth" select="45"/>
  63
  64 <xsl:template name="mksymbol-1">
  65  <xsl:param name="symbol" select="''"/>
  66  <xsl:param name="color" select="''"/>
  67  <xsl:param name="size" select="''"/>
  68   <xsl:choose>
  69    <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
  70     <xsl:variable name="fontsymbol">
  71      <xsl:choose>
  72       <xsl:when test="$symbol = 'forall'">
  73        <xsl:value-of select="'&#x22;'"/>
  74       </xsl:when>
  75       <xsl:when test="$symbol = 'lambda'">
  76        <xsl:value-of select="'l'"/>
  77       </xsl:when>
  78       <xsl:when test="$symbol = 'prod'">
  79        <xsl:value-of select="'&#x00d5;'"/>
  80       </xsl:when>
  81       <xsl:when test="$symbol = 'arrow'">
  82        <xsl:value-of select="'&#x00ae;'"/>
  83       </xsl:when>
  84      </xsl:choose>
  85     </xsl:variable>
  86     <FONT FACE="symbol" SIZE="{$size}" mathcolor="{$color}">
  87      <xsl:value-of select="$fontsymbol"/>
  88     </FONT>
  89    </xsl:when>
  90    <xsl:otherwise>
  91     <xsl:variable name="unicodesymbol">
  92      <xsl:choose>
  93       <xsl:when test="$symbol = 'forall'">
  94        <xsl:value-of select="'&#8704;'"/>
  95       </xsl:when>
  96       <xsl:when test="$symbol = 'lambda'">
  97        <xsl:value-of select="'&#955;'"/>
  98       </xsl:when>
  99       <xsl:when test="$symbol = 'prod'">
 100        <xsl:value-of select="'&#928;'"/>
 101       </xsl:when>
 102       <xsl:when test="$symbol = 'arrow'">
 103        <xsl:value-of select="'&#8594;'"/>
 104       </xsl:when>
 105      </xsl:choose>
 106     </xsl:variable>
 107     <FONT color="{$color}">
 108      <xsl:value-of select="$unicodesymbol"/>
 109     </FONT>
 110    </xsl:otherwise>
 111   </xsl:choose>
 112 </xsl:template>
 113
 114 <xsl:template match="/">
 115  <xsl:param name="current_indent" select="0"/>
 116  <xsl:choose>
 117   <xsl:when test="$type = 'standalone'">
 118    <html>
 119       <head>
 120          <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
 121          <style> A { text-decoration: none } </style>
 122       </head>
 123       <body bgcolor="white">
 124          <xsl:apply-templates>
 125             <xsl:with-param name="current_indent" select="0"/>
 126          </xsl:apply-templates>
 127       </body>
 128    </html>
 129   </xsl:when>
 130   <xsl:otherwise>
 131    <to_be_embedded>
 132     <xsl:apply-templates>
 133      <xsl:with-param name="current_indent" select="0"/>
 134     </xsl:apply-templates>
 135    </to_be_embedded>
 136   </xsl:otherwise>
 137  </xsl:choose>
 138 </xsl:template>
 139
 140 <!--***********************************************************************-->
 141 <!-- Indentation                                                           -->
 142 <!--***********************************************************************-->
 143
 144 <xsl:template name="make_indent">
 145  <xsl:param name="current_indent" select="0"/>
 146   <xsl:if test="$current_indent > 0">
 147    <xsl:text>&#x00a0;</xsl:text>
 148    <xsl:call-template name="make_indent">
 149     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
 150    </xsl:call-template>
 151   </xsl:if>
 152 </xsl:template>
 153
 154 <!-- Syntactic Sugar -->
 155 <xsl:template match="m:type">
 156 <xsl:param name="current_indent" select="0"/>
 157 <xsl:apply-templates>
 158  <xsl:with-param name="current_indent"
 159            select="$current_indent"/>
 160 </xsl:apply-templates>
 161 </xsl:template>
 162
 163 <xsl:template match="m:condition">
 164 <xsl:param name="current_indent" select="0"/>
 165 <xsl:apply-templates>
 166  <xsl:with-param name="current_indent"
 167            select="$current_indent"/>
 168 </xsl:apply-templates>
 169 </xsl:template>
 170
 171 <xsl:template match="m:math">
 172 <xsl:param name="current_indent" select="0"/>
 173 <xsl:apply-templates>
 174  <xsl:with-param name="current_indent"
 175            select="$current_indent"/>
 176 </xsl:apply-templates>
 177 </xsl:template>
 178
 179 <!--*********************************************************************-->
 180 <!--                         INLINE MODE                                 -->
 181 <!--*********************************************************************-->
 182
 183 <!-- href -->
 184 <xsl:template mode="inline" match="m:ci">
 185  <xsl:choose>
 186   <xsl:when test="boolean(@definitionURL)">
 187    <a href="{@definitionURL}">
 188    <xsl:apply-templates/>
 189    </a>
 190   </xsl:when>
 191   <xsl:otherwise>
 192    <xsl:value-of select="."/>
 193   </xsl:otherwise>
 194  </xsl:choose>
 195 </xsl:template>
 196
 197 <!-- CSYMBOL -->
 198
 199 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 200    <xsl:variable name="name">
 201     <xsl:value-of select="m:csymbol"/>
 202    </xsl:variable>
 203    <xsl:choose>
 204     <!-- FORALL -->
 205     <xsl:when test="$name='forall'">
 206      <xsl:call-template name="mksymbol-1">
 207       <xsl:with-param name="symbol" select="$name"/>
 208       <xsl:with-param name="color" select="'blue'"/>
 209       <xsl:with-param name="size" select="'+2'"/>
 210      </xsl:call-template>
 211      <xsl:apply-templates select="m:bvar/m:ci"/>
 212      <xsl:text>:</xsl:text>
 213      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 214      <xsl:text>.</xsl:text>
 215      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 216     </xsl:when>
 217     <xsl:when test="$name='prod'">
 218      <xsl:call-template name="mksymbol-1">
 219       <xsl:with-param name="symbol" select="$name"/>
 220       <xsl:with-param name="color" select="'blue'"/>
 221       <xsl:with-param name="size" select="'+2'"/>
 222      </xsl:call-template>
 223      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 224      <xsl:text>:</xsl:text>
 225      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 226      <xsl:text>.</xsl:text>
 227      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 228     </xsl:when>
 229     <!-- ARROW -->
 230     <xsl:when test="$name='arrow'">
 231      <xsl:text>(</xsl:text>
 232      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 233      <xsl:call-template name="mksymbol-1">
 234       <xsl:with-param name="symbol" select="$name"/>
 235       <xsl:with-param name="color" select="'blue'"/>
 236       <xsl:with-param name="size" select="'+0'"/>
 237      </xsl:call-template>
 238      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 239      <xsl:text>)</xsl:text>
 240     </xsl:when>
 241     <!-- APP -->
 242     <xsl:when test="$name='app'">
 243      <xsl:text>(</xsl:text>
 244      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 245      <xsl:for-each select="*[position()>2]">
 246       <xsl:text>&#x00A0;</xsl:text>
 247       <xsl:apply-templates mode="inline" select="."/>
 248      </xsl:for-each>
 249      <xsl:text>)</xsl:text>
 250     </xsl:when>
 251     <!-- CAST -->
 252     <xsl:when test="$name='cast'">
 253      <xsl:text>(</xsl:text>
 254      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 255      <xsl:text>:></xsl:text>
 256      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 257      <xsl:text>)</xsl:text>
 258     </xsl:when>
 259     <xsl:when test="$name='Prop'">
 260      <FONT color="violet">Prop</FONT>
 261     </xsl:when>
 262     <xsl:when test="$name='Set'">
 263      <FONT color="violet">Set</FONT>
 264     </xsl:when>
 265     <xsl:when test="$name='Type'">
 266      <FONT color="violet">Type</FONT>
 267     </xsl:when>
 268     <!-- MUTCASE -->
 269     <xsl:when test="$name='mutcase'">
 270      <xsl:text>&lt;</xsl:text>
 271      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 272      <xsl:text>&gt; </xsl:text>
 273      <FONT color="red">CASE </FONT>
 274      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 275      <FONT color="red"> OF </FONT>
 276      <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 277       <xsl:choose>
 278        <xsl:when test="not(position() = 1)">
 279         <xsl:text> | </xsl:text>
 280        </xsl:when>
 281       </xsl:choose>
 282       <xsl:apply-templates mode="inline" select="."/>
 283       <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
 284       <xsl:apply-templates mode="inline"
 285            select="following-sibling::*[position()= 1]"/>
 286      </xsl:for-each>
 287     </xsl:when>
 288     <!-- FIX -->
 289     <xsl:when test="$name='fix'">
 290      <FONT color="red">FIX</FONT>
 291      <xsl:value-of select="m:ci"/>
 292      <xsl:text>{</xsl:text>
 293      <xsl:for-each select="m:bvar">
 294       <xsl:value-of select="m:ci"/>
 295       <xsl:text>:</xsl:text>
 296       <xsl:apply-templates mode="inline" select="m:type"/>
 297       <xsl:text>:=</xsl:text>
 298       <xsl:apply-templates mode="inline"
 299              select="following-sibling::*[position() = 1]"/>
 300       <xsl:choose>
 301        <xsl:when test="position()=last()">
 302         <xsl:text>}</xsl:text>
 303        </xsl:when>
 304        <xsl:otherwise>
 305         <xsl:text>;</xsl:text>
 306        </xsl:otherwise>
 307       </xsl:choose>
 308      </xsl:for-each>
 309     </xsl:when>
 310     <!-- COFIX -->
 311     <xsl:when test="$name='cofix'">
 312      <xsl:text>COFIX</xsl:text>
 313      <xsl:value-of select="m:ci"/>
 314      <xsl:text>{</xsl:text>
 315      <xsl:for-each select="m:bvar">
 316       <xsl:value-of select="m:ci"/>
 317       <xsl:text>:</xsl:text>
 318       <xsl:apply-templates mode="inline" select="m:type"/>
 319       <xsl:text>:=</xsl:text>
 320       <xsl:apply-templates mode="inline"
 321           select="following-sibling::*[position() = 1]"/>
 322       <xsl:choose>
 323        <xsl:when test="position()=last()">
 324         <xsl:text>}</xsl:text>
 325        </xsl:when>
 326        <xsl:otherwise>
 327         <xsl:text>;</xsl:text>
 328        </xsl:otherwise>
 329       </xsl:choose>
 330      </xsl:for-each>
 331     </xsl:when>
 332     <!-- proof -->
 333     <xsl:when test="$name='proof'">
 334        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 335        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 336        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 337     </xsl:when>
 338     <!-- false_ind -->
 339     <xsl:when test="$name='false_ind'">
 340     <xsl:apply-templates mode="inline" select="*[3]"/>
 341     <FONT color="red">Contradiction.</FONT>
 342     </xsl:when>
 343     <!-- and_ind -->
 344     <xsl:when test="$name='and_ind'">
 345      <FONT color="red">From&#x00a0;</FONT>
 346      <xsl:apply-templates select="*[2]"/>
 347      <FONT color="red">&#x00a0;we get</FONT>
 348      (
 349      <xsl:apply-templates select="*[3]"/>
 350      )&#x00a0;
 351      <xsl:apply-templates mode="inline" select="*[4]"/>
 352      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 353      (
 354      <xsl:apply-templates select="*[5]"/>
 355      )&#x00a0;
 356      <xsl:apply-templates mode="inline" select="*[6]"/>
 357      ;
 358      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 359      <xsl:apply-templates mode="inline" select="*[7]"/>
 360     </xsl:when>
 361
 362        <xsl:when test="$name='subst'">
 363        <xsl:apply-templates select="*[3]" mode="inline"/>
 364        <xsl:text>[</xsl:text>
 365        <xsl:apply-templates select="*[4]" mode="inline"/>
 366        <a href="{*[1]/@definitionURL}">
 367        <FONT color="green" FACE="symbol">
 368         <xsl:text>&#x00ac;</xsl:text>
 369        </FONT>
 370        </a>
 371        <xsl:apply-templates select="*[2]" mode="inline"/>
 372        <xsl:text>]</xsl:text>
 373       </xsl:when>
 374
 375       <xsl:when test="$name='lift_with_base'">
 376        <SUB>
 377        <xsl:apply-templates select="*[3]" mode="inline"/>
 378        </SUB>
 379        <a href="{*[1]/@definitionURL}">
 380        <FONT color="green" FACE="symbol">
 381         <xsl:text>&#x00ad;</xsl:text>
 382        </FONT>
 383        </a>
 384        <SUP>
 385        <xsl:apply-templates select="*[4]" mode="inline"/>
 386        </SUP>
 387        <xsl:text>(</xsl:text>
 388        <xsl:apply-templates select="*[2]" mode="inline"/>
 389        <xsl:text>)</xsl:text>
 390       </xsl:when>
 391
 392       <xsl:when test="$name='lift'">
 393        <a href="{*[1]/@definitionURL}">
 394        <FONT color="green" FACE="symbol">
 395         <xsl:text>&#x00ad;</xsl:text>
 396        </FONT>
 397        </a>
 398        <SUP>
 399        <xsl:apply-templates select="*[2]" mode="inline"/>
 400        </SUP>
 401        <xsl:text>(</xsl:text>
 402        <xsl:apply-templates select="*[3]" mode="inline"/>
 403        <xsl:text>)</xsl:text>
 404       </xsl:when>
 405
 406       <!-- reduction -->
 407       <xsl:when test="$name='beta_red1'">
 408        <xsl:apply-templates select="*[2]" mode="inline"/>
 409        <a href="{*[1]/@definitionURL}">
 410        <FONT color="green" FACE="symbol">
 411         <xsl:text>&#x00ae;</xsl:text>
 412        </FONT>
 413        <SUB>
 414         <FONT color="green" FACE="symbol">
 415          <xsl:text>&#x0062;</xsl:text>
 416         </FONT>
 417        </SUB>
 418        </a>
 419        <xsl:apply-templates select="*[3]" mode="inline"/>
 420       </xsl:when>
 421
 422       <xsl:when test="$name='beta_red'">
 423        <xsl:apply-templates select="*[2]" mode="inline"/>
 424        <a href="{*[1]/@definitionURL}">
 425        <FONT color="green" FACE="symbol">
 426         <xsl:text>&#x00ae;</xsl:text>
 427        </FONT>
 428        <SUB>
 429         <FONT color="green" FACE="symbol">
 430          <xsl:text>&#x0062;*</xsl:text>
 431         </FONT>
 432        </SUB>
 433        </a>
 434        <xsl:apply-templates select="*[3]" mode="inline"/>
 435       </xsl:when>
 436
 437       <xsl:when test="$name='par_beta_red1'">
 438        <xsl:apply-templates select="*[2]" mode="inline"/>
 439        <a href="{*[1]/@definitionURL}">
 440        <FONT color="green" FACE="symbol">
 441         <xsl:text>&#x00de;</xsl:text>
 442        </FONT>
 443        <SUB>
 444         <FONT color="green" FACE="symbol">
 445          <xsl:text>&#x0062;</xsl:text>
 446         </FONT>
 447        </SUB>
 448        </a>
 449        <xsl:apply-templates select="*[3]" mode="inline"/>
 450       </xsl:when>
 451
 452       <xsl:when test="$name='par_beta_red'">
 453        <xsl:apply-templates select="*[2]" mode="inline"/>
 454        <a href="{*[1]/@definitionURL}">
 455        <FONT color="green" FACE="symbol">
 456         <xsl:text>&#x00de;</xsl:text>
 457        </FONT>
 458        <SUB>
 459         <FONT color="green" FACE="symbol">
 460          <xsl:text>&#x0062;*</xsl:text>
 461         </FONT>
 462        </SUB>
 463        </a>
 464        <xsl:apply-templates select="*[3]" mode="inline"/>
 465       </xsl:when>
 466
 467       <!-- forgetful -->
 468       <xsl:when test="$name='forgetful'">
 469        <a href="{*[1]/@definitionURL}">|</a>
 470        <xsl:apply-templates select="*[2]" mode="inline"/>
 471        <a href="{*[1]/@definitionURL}">|</a>
 472       </xsl:when>
 473
 474       <!-- boolean algebra of redexes -->
 475
 476       <!-- isomorphic -->
 477       <xsl:when test="$name='isomorphic'">
 478        <xsl:apply-templates select="*[2]" mode="inline"/>
 479        <a href="{*[1]/@definitionURL}">
 480         <FONT color="green" FACE="symbol">
 481         <xsl:text>&#x0040;</xsl:text>
 482        </FONT>
 483        </a>
 484        <xsl:apply-templates select="*[3]" mode="inline"/>
 485       </xsl:when>
 486
 487       <!-- INTERP -->
 488       <xsl:when test="$name='interp'">
 489          <font color="green">[</font>
 490             <xsl:apply-templates select="*[2]"/>
 491          <font color="green">]</font>
 492       </xsl:when>
 493
 494    </xsl:choose>
 495 </xsl:template>
 496
 497 <xsl:template mode="inline" match="m:lambda">
 498       <xsl:call-template name="mksymbol-1">
 499        <xsl:with-param name="symbol" select="'lambda'"/>
 500        <xsl:with-param name="color" select="'red'"/>
 501        <xsl:with-param name="size" select="'+2'"/>
 502       </xsl:call-template>
 503       <xsl:apply-templates select="m:bvar/m:ci"/>
 504       <xsl:text>:</xsl:text>
 505       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 506       <xsl:text>.</xsl:text>
 507       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 508 </xsl:template>
 509
 510 <!--*********************************************************************-->
 511 <!--                       COUNTING MODE                                 -->
 512 <!--*********************************************************************-->
 513
 514 <xsl:template match="m:apply[m:csymbol]">
 515   <xsl:param name="current_indent" select="0"/>
 516   <xsl:param name="width" select="$framewidth"/>
 517   <xsl:variable name="name">
 518    <xsl:value-of select="m:csymbol"/>
 519   </xsl:variable>
 520   <xsl:variable name="charlength">
 521    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 522   </xsl:variable>
 523      <!-- <xsl:value-of select="$current_indent"/> -->
 524      <!-- <xsl:value-of select="$charlength"/> -->
 525      <xsl:choose>
 526      <!-- FORALL -->
 527       <xsl:when test="$name='forall'">
 528        <xsl:choose>
 529        <xsl:when test="$charlength > $framewidth">
 530          <!-- &#x03a0; -->
 531          <xsl:call-template name="mksymbol-1">
 532           <xsl:with-param name="symbol" select="$name"/>
 533           <xsl:with-param name="color" select="'blue'"/>
 534           <xsl:with-param name="size" select="'+2'"/>
 535          </xsl:call-template>
 536          <xsl:apply-templates select="m:bvar/m:ci"/>
 537          <xsl:text>:</xsl:text>
 538          <xsl:apply-templates select="m:bvar/m:type">
 539           <xsl:with-param name="current_indent"
 540            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 541          </xsl:apply-templates>
 542          <br/>
 543          <xsl:call-template name="make_indent">
 544           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 545          </xsl:call-template>
 546          <xsl:text>.</xsl:text>
 547          <xsl:apply-templates select="*[position()=3]">
 548           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 549          </xsl:apply-templates>
 550        </xsl:when>
 551        <xsl:otherwise>
 552         <xsl:apply-templates mode="inline" select="."/>
 553        </xsl:otherwise>
 554        </xsl:choose>
 555       </xsl:when>
 556       <!-- PROD -->
 557       <xsl:when test="$name='prod'">
 558        <xsl:choose>
 559        <xsl:when test="$charlength > $framewidth">
 560          <xsl:call-template name="mksymbol-1">
 561           <xsl:with-param name="symbol" select="$name"/>
 562           <xsl:with-param name="color" select="'blue'"/>
 563           <xsl:with-param name="size" select="'+2'"/>
 564          </xsl:call-template>
 565          <xsl:apply-templates select="m:bvar/m:ci"/>
 566          <xsl:text>:</xsl:text>
 567          <xsl:apply-templates select="m:bvar/m:type">
 568           <xsl:with-param name="current_indent"
 569            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 570          </xsl:apply-templates><br/>
 571          <xsl:call-template name="make_indent">
 572           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 573          </xsl:call-template>
 574          <xsl:text>.</xsl:text>
 575          <xsl:apply-templates select="*[position()=3]">
 576           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 577          </xsl:apply-templates>
 578        </xsl:when>
 579        <xsl:otherwise>
 580         <xsl:apply-templates mode="inline" select="."/>
 581        </xsl:otherwise>
 582        </xsl:choose>
 583       </xsl:when>
 584       <!-- ARROW -->
 585       <xsl:when test="$name='arrow'">
 586        <xsl:choose>
 587        <xsl:when test="$charlength > $framewidth">
 588        <xsl:text>(</xsl:text>
 589        <xsl:apply-templates select="*[position()=2]">
 590         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 591        </xsl:apply-templates>
 592        <br/>
 593        <xsl:call-template name="make_indent">
 594         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 595        </xsl:call-template>
 596        <!-- -> -->
 597        <xsl:call-template name="mksymbol-1">
 598         <xsl:with-param name="symbol" select="$name"/>
 599         <xsl:with-param name="color" select="'blue'"/>
 600         <xsl:with-param name="size" select="'+2'"/>
 601        </xsl:call-template>
 602        <xsl:apply-templates select="*[position()=3]">
 603         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 604        </xsl:apply-templates>
 605        <xsl:text>)</xsl:text>
 606        </xsl:when>
 607        <xsl:otherwise>
 608         <xsl:apply-templates mode="inline" select="."/>
 609        </xsl:otherwise>
 610        </xsl:choose>
 611       </xsl:when>
 612       <!-- APP -->
 613       <xsl:when test="$name='app'">
 614        <xsl:choose>
 615        <xsl:when test="$charlength  > $framewidth">
 616         <xsl:text>(</xsl:text>
 617         <xsl:apply-templates select="*[position()=2]">
 618          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 619         </xsl:apply-templates>
 620          <xsl:for-each select="*[position()>2]">
 621           <br/>
 622            <xsl:call-template name="make_indent">
 623             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 624            </xsl:call-template>
 625             <xsl:apply-templates select=".">
 626              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 627             </xsl:apply-templates>
 628          </xsl:for-each>
 629          <xsl:text>)</xsl:text>
 630        </xsl:when>
 631        <xsl:otherwise>
 632         <xsl:apply-templates mode="inline" select="."/>
 633        </xsl:otherwise>
 634        </xsl:choose>
 635       </xsl:when>
 636       <xsl:when test="$name='cast'">
 637        <xsl:choose>
 638         <xsl:when test="$showcast = 1">
 639          <xsl:choose>
 640           <xsl:when test="$charlength > $framewidth">
 641            <xsl:text>(</xsl:text>
 642            <xsl:apply-templates select="*[position()=2]">
 643             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 644            </xsl:apply-templates><br/>
 645            <xsl:call-template name="make_indent">
 646             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 647            <xsl:text>:></xsl:text>
 648            <xsl:apply-templates select="*[position()=3]">
 649             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 650            </xsl:apply-templates>
 651            <xsl:text>)</xsl:text>
 652           </xsl:when>
 653           <xsl:otherwise>
 654            <xsl:apply-templates mode="inline" select="."/>
 655           </xsl:otherwise>
 656          </xsl:choose>
 657         </xsl:when>
 658         <xsl:otherwise>
 659          <xsl:apply-templates select="*[position()=2]">
 660           <xsl:with-param name="current_indent" select="$current_indent"/>
 661          </xsl:apply-templates>
 662         </xsl:otherwise>
 663        </xsl:choose>
 664       </xsl:when>
 665       <xsl:when test="$name='Prop'">
 666        <xsl:text>Prop</xsl:text>
 667       </xsl:when>
 668       <xsl:when test="$name='Set'">
 669        <xsl:text>Set</xsl:text>
 670       </xsl:when>
 671       <xsl:when test="$name='Type'">
 672        <xsl:text>Type</xsl:text>
 673       </xsl:when>
 674       <xsl:when test="$name='mutcase'">
 675        <xsl:choose>
 676        <xsl:when test="$charlength > $framewidth">
 677          <xsl:text>&lt;</xsl:text>
 678          <xsl:apply-templates select="*[position()=2]">
 679           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 680          </xsl:apply-templates>
 681          <xsl:text>&gt; </xsl:text>
 682          <br/>
 683          <xsl:call-template name="make_indent">
 684           <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
 685          <xsl:text>CASE </xsl:text>
 686          <xsl:apply-templates select="*[position()=3]">
 687           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 688          </xsl:apply-templates>
 689          <xsl:text> OF </xsl:text>
 690          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 691          <br/>
 692          <xsl:call-template name="make_indent">
 693           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 694          </xsl:call-template>
 695             <xsl:choose>
 696             <xsl:when test="position() = 1">
 697              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 698             </xsl:when>
 699             <xsl:otherwise>
 700              <xsl:text>| </xsl:text>
 701             </xsl:otherwise>
 702             </xsl:choose>
 703             <xsl:apply-templates select="."/>
 704             <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
 705             <xsl:variable name="body_size">
 706              <xsl:apply-templates
 707               select="following-sibling::*[1]/*[1]" mode="charcount"/>
 708             </xsl:variable>
 709             <xsl:choose>
 710              <xsl:when test="$body_size > $framewidth">
 711               <br/>
 712               <xsl:call-template name="make_indent">
 713                <xsl:with-param name="current_indent"
 714                     select="$current_indent + 8"/>
 715               </xsl:call-template>
 716               <xsl:apply-templates
 717                    select="following-sibling::*[position()= 1]">
 718               <xsl:with-param name="current_indent"
 719                    select="$current_indent + 8"/>
 720              </xsl:apply-templates>
 721             </xsl:when>
 722             <xsl:otherwise>
 723              <xsl:apply-templates select="following-sibling::*[position()= 1]"
 724                    mode="inline" />
 725             </xsl:otherwise>
 726            </xsl:choose>
 727          </xsl:for-each>
 728        </xsl:when>
 729        <xsl:otherwise>
 730         <xsl:apply-templates mode="inline" select="."/>
 731        </xsl:otherwise>
 732        </xsl:choose>
 733       </xsl:when>
 734       <!-- FIX -->
 735       <xsl:when test="$name='fix'">
 736        <xsl:choose>
 737        <xsl:when test="$charlength  > $framewidth">
 738             <xsl:text>FIX</xsl:text>
 739             <xsl:value-of select="m:ci"/>
 740             <xsl:text>{</xsl:text>
 741             <xsl:for-each select="m:bvar">
 742               <br/>
 743               <xsl:call-template name="make_indent">
 744                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 745               </xsl:call-template>
 746               <xsl:value-of select="m:ci"/>
 747               <xsl:text>:</xsl:text>
 748               <xsl:apply-templates select="m:type">
 749                <xsl:with-param name="current_indent"
 750                     select="$current_indent + 5 + string-length(m:ci)"/>
 751                </xsl:apply-templates>
 752               <br/>
 753               <xsl:call-template name="make_indent">
 754                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 755               </xsl:call-template>
 756               <xsl:text>:=</xsl:text>
 757               <xsl:apply-templates select="following-sibling::*[position() = 1]">
 758                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 759               </xsl:apply-templates>
 760             </xsl:for-each>
 761              <br/>
 762               <xsl:call-template name="make_indent">
 763                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 764               </xsl:call-template>
 765            <xsl:text>}</xsl:text>
 766        </xsl:when>
 767        <xsl:otherwise>
 768         <xsl:apply-templates mode="inline" select="."/>
 769        </xsl:otherwise>
 770        </xsl:choose>
 771       </xsl:when>
 772       <!-- COFIX -->
 773       <xsl:when test="$name='cofix'">
 774        <xsl:choose>
 775        <xsl:when test="($charlength + 10) > $framewidth">
 776             <xsl:text>COFIX</xsl:text>
 777             <xsl:value-of select="m:ci"/>
 778             <xsl:text>{</xsl:text>
 779             <br/>
 780             <xsl:call-template name="make_indent">
 781              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 782             </xsl:call-template>
 783             <xsl:for-each select="m:bvar">
 784                 <xsl:value-of select="m:ci"/>
 785                 <xsl:text>:</xsl:text>
 786                 <xsl:apply-templates select="m:type">
 787                  <xsl:with-param name="current_indent"
 788                     select="$current_indent + 5 + string-length(m:ci)"/>
 789                 </xsl:apply-templates>
 790                 <br/>
 791                 <xsl:call-template name="make_indent">
 792                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 793                 </xsl:call-template>
 794                 <xsl:text>:=</xsl:text>
 795                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 796                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 797                 </xsl:apply-templates>
 798
 799             </xsl:for-each>
 800             <br/>
 801               <xsl:call-template name="make_indent">
 802                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 803               </xsl:call-template>
 804             <xsl:text>}</xsl:text>
 805        </xsl:when>
 806        <xsl:otherwise>
 807         <xsl:apply-templates mode="inline" select="m:type"/>
 808        </xsl:otherwise>
 809        </xsl:choose>
 810       </xsl:when>
 811       <xsl:when test="$name='let_in'">
 812        <xsl:text>let&#x00a0;</xsl:text>
 813        <xsl:apply-templates select="m:bvar/m:ci"/>
 814        <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
 815        <xsl:apply-templates select="*[3]">
 816         <xsl:with-param name="current_indent" select="$current_indent+14"/>
 817        </xsl:apply-templates>
 818        <br/>
 819        <xsl:call-template name="make_indent">
 820         <xsl:with-param name="current_indent" select="$current_indent"/>
 821        </xsl:call-template>
 822        <xsl:text>in&#x00a0;</xsl:text>
 823        <xsl:apply-templates select="*[4]">
 824         <xsl:with-param name="current_indent" select="$current_indent+5"/>
 825        </xsl:apply-templates>
 826       </xsl:when>
 827
 828       <!-- ***************************************** -->
 829       <!-- *********** PROOF ELEMENTS ************** -->
 830       <!-- ***************************************** -->
 831       <!-- PROOF -->
 832       <xsl:when test="$name='proof'">
 833        <xsl:apply-templates select="*[position()=2]">
 834         <xsl:with-param name="current_indent" select="$current_indent"/>
 835        </xsl:apply-templates>
 836        <br/>
 837        <!-- <xsl:element name="br"/> -->
 838        <xsl:call-template name="make_indent">
 839         <xsl:with-param name="current_indent" select="$current_indent"/>
 840        </xsl:call-template>
 841        <FONT color="red">we proved&#x00a0;</FONT>
 842        <xsl:apply-templates select="*[position()=3]">
 843         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 844        </xsl:apply-templates>
 845       </xsl:when>
 846       <!-- letin1 -->
 847       <xsl:when test="$name='letin1'">
 848        <xsl:apply-templates select="*[position()=2]">
 849         <xsl:with-param name="current_indent" select="$current_indent"/>
 850        </xsl:apply-templates>
 851        <br/>
 852        <xsl:call-template name="make_indent">
 853         <xsl:with-param name="current_indent" select="$current_indent"/>
 854        </xsl:call-template>
 855        <xsl:apply-templates select="*[position()=3]">
 856         <xsl:with-param name="current_indent" select="$current_indent"/>
 857        </xsl:apply-templates>
 858       </xsl:when>
 859       <!-- letin -->
 860       <xsl:when test="$name='letin'">
 861        <xsl:for-each select="*[position()>1 and last()>position()]">
 862         <xsl:apply-templates select=".">
 863          <xsl:with-param name="current_indent" select="$current_indent"/>
 864         </xsl:apply-templates>
 865         <br/>
 866         <xsl:call-template name="make_indent">
 867          <xsl:with-param name="current_indent" select="$current_indent"/>
 868         </xsl:call-template>
 869        </xsl:for-each>
 870        <xsl:apply-templates select="*[position()=last()]">
 871         <xsl:with-param name="current_indent" select="$current_indent"/>
 872        </xsl:apply-templates>
 873       </xsl:when>
 874       <!-- Let -->
 875       <xsl:when test="$name='let'">
 876        (
 877        <xsl:apply-templates select="m:ci"/>
 878        )
 879        <xsl:apply-templates select="*[3]">
 880         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 881        </xsl:apply-templates>
 882       </xsl:when>
 883       <!-- rw_step -->
 884       <xsl:when test="$name='rw_step'">
 885        <xsl:choose>
 886         <xsl:when test="name(*[2])='m:apply'">
 887          <xsl:apply-templates select="*[2]">
 888           <xsl:with-param name="current_indent" select="$current_indent"/>
 889          </xsl:apply-templates>
 890         </xsl:when>
 891         <xsl:otherwise>
 892          <FONT color="red">Consider&#x00a0;</FONT>
 893          <xsl:apply-templates select="*[2]"/>
 894         </xsl:otherwise>
 895        </xsl:choose>
 896        <xsl:variable name="charlength_first">
 897         <xsl:apply-templates select="*[3]/*[1]" mode="charcount"/>
 898        </xsl:variable>
 899        <xsl:variable name="charlength_second">
 900         <xsl:apply-templates select="*[4]/*[1]" mode="charcount"/>
 901        </xsl:variable>
 902        <xsl:variable name="charlength_side_proof">
 903         <xsl:apply-templates select="*[5]/*[1]" mode="charcount"/>
 904        </xsl:variable>
 905        <xsl:variable name="split1"
 906           select="$charlength_first + $charlength_second > $framewidth"/>
 907        <xsl:variable name="split2"
 908           select="$charlength_second + $charlength_side_proof > $framewidth"/>
 909      <!-- <xsl:value-of select="$current_indent"/> -->
 910      <!-- <xsl:value-of select="$charlength"/> -->
 911        <br/>
 912        <xsl:call-template name="make_indent">
 913         <xsl:with-param name="current_indent" select="$current_indent"/>
 914        </xsl:call-template>
 915        <FONT color="red">Rewrite&#x00a0;</FONT>
 916        <xsl:apply-templates mode="inline" select="*[3]"/>
 917        <xsl:text>&#x00a0;</xsl:text>
 918        <xsl:if test="$split1">
 919        <br/>
 920        <xsl:call-template name="make_indent">
 921         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 922        </xsl:call-template>
 923        </xsl:if>
 924        <FONT color="red">with&#x00a0;</FONT>
 925        <xsl:apply-templates mode="inline" select="*[4]"/>
 926        <xsl:text>&#x00a0;</xsl:text>
 927        <xsl:if test="$split2">
 928        <br/>
 929        <xsl:call-template name="make_indent">
 930         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 931        </xsl:call-template>
 932        </xsl:if>
 933        <FONT color="red">by&#x00a0;</FONT>
 934        <xsl:apply-templates select="*[5]">
 935         <xsl:with-param name="current_indent" select="$current_indent+7"/>
 936        </xsl:apply-templates>
 937       </xsl:when>
 938       <!-- rewrite and apply -->
 939       <xsl:when test="$name='rewrite_and_apply'">
 940        <xsl:apply-templates select="*[2]">
 941         <xsl:with-param name="current_indent" select="$current_indent"/>
 942        </xsl:apply-templates>
 943        <br/>
 944        <xsl:call-template name="make_indent">
 945         <xsl:with-param name="current_indent" select="$current_indent"/>
 946        </xsl:call-template>
 947        <FONT color="red">Then apply it to&#x00a0;</FONT>
 948        <xsl:apply-templates select="*[position()>2]"/>
 949       </xsl:when>
 950       <!-- by_induction -->
 951       <xsl:when test="$name='by_induction'">
 952        <FONT color="red">We prove&#x00a0;</FONT>
 953        <xsl:apply-templates select="../*[3]">
 954         <xsl:with-param name="current_indent" select="$current_indent+18"/>
 955        </xsl:apply-templates>
 956        <br/>
 957        <xsl:call-template name="make_indent">
 958         <xsl:with-param name="current_indent" select="$current_indent"/>
 959        </xsl:call-template>
 960        <FONT color="red">by induction on&#x00a0;</FONT>
 961        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
 962         <xsl:with-param name="current_indent" select="$current_indent+30"/>
 963        </xsl:apply-templates>
 964        <!--
 965        <br/>
 966        <xsl:call-template name="make_indent">
 967         <xsl:with-param name="current_indent" select="$current_indent"/>
 968        </xsl:call-template>
 969        <xsl:text>The induction property is</xsl:text>
 970        <br/>
 971        <xsl:call-template name="make_indent">
 972         <xsl:with-param name="current_indent" select="$current_indent"/>
 973        </xsl:call-template>
 974        <xsl:apply-templates select="*[3]">
 975         <xsl:with-param name="current_indent" select="$current_indent"/>
 976        </xsl:apply-templates>
 977        -->
 978        <xsl:apply-templates
 979             select="*[position()>3 and not(position()=last())]">
 980         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 981        </xsl:apply-templates>
 982        <!-- <br/>
 983        <xsl:call-template name="make_indent">
 984         <xsl:with-param name="current_indent" select="$current_indent"/>
 985        </xsl:call-template>
 986        <xsl:text>End induction</xsl:text> -->
 987       </xsl:when>
 988       <!-- inductive_case -->
 989       <xsl:when test="$name='inductive_case'">
 990        <br/>
 991        <xsl:call-template name="make_indent">
 992         <xsl:with-param name="current_indent" select="$current_indent"/>
 993        </xsl:call-template>
 994        <FONT color="red">Case&#x00a0;</FONT>
 995        <xsl:apply-templates select="*[2]">
 996         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 997        </xsl:apply-templates>
 998        <xsl:if test="*[3]/*[position()>1]">
 999         <br/>
1000         <xsl:call-template name="make_indent">
1001          <xsl:with-param name="current_indent" select="$current_indent+4"/>
1002         </xsl:call-template>
1003         <FONT color="red">By induction hypothesis, we have:</FONT>
1004         <xsl:for-each select="*[3]/*[position()>1]">
1005          <br/>
1006          <xsl:call-template name="make_indent">
1007           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1008          </xsl:call-template>
1009          <xsl:text>(</xsl:text>
1010          <xsl:apply-templates select="m:ci"/>
1011          <xsl:text>)&#x00a0;</xsl:text>
1012          <xsl:apply-templates select="m:type">
1013           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1014          </xsl:apply-templates>
1015         </xsl:for-each>
1016        </xsl:if>
1017        <br/>
1018         <xsl:call-template name="make_indent">
1019          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1020         </xsl:call-template>
1021        <xsl:apply-templates select="*[4]">
1022         <xsl:with-param name="current_indent" select="$current_indent +4"/>
1023        </xsl:apply-templates>
1024        <!-- <br/>
1025        <xsl:call-template name="make_indent">
1026         <xsl:with-param name="current_indent" select="$current_indent"/>
1027        </xsl:call-template>
1028        <xsl:text>End Case</xsl:text> -->
1029       </xsl:when>
1030       <!-- case_lhs  -->
1031       <xsl:when test="$name='case_lhs'">
1032        <xsl:choose>
1033         <xsl:when test="count(*)=2">
1034          <xsl:apply-templates mode="inline" select="*[2]"/>
1035         </xsl:when>
1036         <xsl:otherwise>
1037          <xsl:text>(</xsl:text>
1038          <xsl:apply-templates mode="inline" select="*[2]"/>
1039          <xsl:for-each select="m:bvar">
1040           <xsl:text>&#x00a0;</xsl:text>
1041           <xsl:apply-templates mode="inline" select="*[1]"/>
1042           <xsl:text>:</xsl:text>
1043           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1044          </xsl:for-each>
1045          <xsl:text>)</xsl:text>
1046         </xsl:otherwise>
1047        </xsl:choose>
1048       </xsl:when>
1049       <!-- nat_ind -->
1050       <xsl:when test="$name='nat_ind_complete'">
1051        <FONT color="red">By induction on&#x00a0;</FONT>
1052        <xsl:apply-templates select="*[2]"/>:
1053        <br/>
1054        <xsl:call-template name="make_indent">
1055         <xsl:with-param name="current_indent" select="$current_indent"/>
1056        </xsl:call-template>
1057        <xsl:text>0&#x00a0;</xsl:text>
1058        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
1059        <xsl:apply-templates select="*[3]">
1060         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1061        </xsl:apply-templates>
1062        <br/>
1063        <xsl:call-template name="make_indent">
1064         <xsl:with-param name="current_indent" select="$current_indent"/>
1065        </xsl:call-template>
1066        <xsl:text>S(</xsl:text>
1067        <xsl:apply-templates select="*[4]"/>
1068        <xsl:text>)&#x00a0;</xsl:text>
1069        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
1070        <FONT color="red">Assume by induction</FONT>
1071        <br/>
1072        <xsl:call-template name="make_indent">
1073         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1074        </xsl:call-template>
1075        <xsl:text>(</xsl:text>
1076        <xsl:apply-templates select="*[5]"/>
1077        <xsl:text>)</xsl:text>
1078        <xsl:apply-templates select="*[6]">
1079         <xsl:with-param name="current_indent" select="$current_indent + 14"/>
1080        </xsl:apply-templates>
1081        <br/>
1082        <xsl:call-template name="make_indent">
1083         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1084        </xsl:call-template>
1085        <xsl:apply-templates select="*[7]">
1086         <xsl:with-param name="current_indent" select="$current_indent + 10"/>
1087        </xsl:apply-templates>
1088       </xsl:when>
1089       <!-- false_ind -->
1090       <xsl:when test="$name='false_ind'">
1091        <xsl:apply-templates select="*[3]">
1092         <xsl:with-param name="current_indent" select="$current_indent"/>
1093        </xsl:apply-templates>
1094        <br/>
1095        <xsl:call-template name="make_indent">
1096         <xsl:with-param name="current_indent" select="$current_indent"/>
1097        </xsl:call-template>
1098        <FONT color="red">Contradiction.</FONT>
1099       </xsl:when>
1100       <!-- and_ind -->
1101       <xsl:when test="$name='and_ind'">
1102        <xsl:choose>
1103         <xsl:when test="name(*[2])='m:apply'">
1104          <xsl:apply-templates select="*[2]">
1105           <xsl:with-param name="current_indent" select="$current_indent"/>
1106          </xsl:apply-templates>
1107         </xsl:when>
1108         <xsl:otherwise>
1109          <FONT color="red">Consider&#x00a0;</FONT>
1110          <xsl:apply-templates select="*[2]"/>
1111         </xsl:otherwise>
1112        </xsl:choose>
1113        <br/>
1114        <xsl:call-template name="make_indent">
1115         <xsl:with-param name="current_indent" select="$current_indent"/>
1116        </xsl:call-template>
1117        <FONT color="red">In particular, we have</FONT>
1118        <br/>
1119        <xsl:call-template name="make_indent">
1120         <xsl:with-param name="current_indent" select="$current_indent"/>
1121        </xsl:call-template>
1122        (
1123        <xsl:apply-templates select="*[3]"/>
1124        )&#x00a0;
1125        <xsl:apply-templates select="*[4]">
1126         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1127        </xsl:apply-templates>
1128        <br/>
1129        <xsl:call-template name="make_indent">
1130         <xsl:with-param name="current_indent" select="$current_indent"/>
1131        </xsl:call-template>
1132        (
1133        <xsl:apply-templates select="*[5]"/>
1134        )&#x00a0;
1135        <xsl:apply-templates select="*[6]">
1136         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1137        </xsl:apply-templates>
1138        <br/>
1139        <xsl:call-template name="make_indent">
1140         <xsl:with-param name="current_indent" select="$current_indent"/>
1141        </xsl:call-template>
1142        <xsl:apply-templates select="*[7]">
1143         <xsl:with-param name="current_indent" select="$current_indent"/>
1144        </xsl:apply-templates>
1145       </xsl:when>
1146       <!-- full_or_ind -->
1147       <xsl:when test="$name='full_or_ind'">
1148        <xsl:choose>
1149         <xsl:when test="name(*[2])='m:apply'">
1150          <xsl:apply-templates select="*[2]">
1151           <xsl:with-param name="current_indent" select="$current_indent"/>
1152          </xsl:apply-templates>
1153         </xsl:when>
1154         <xsl:otherwise>
1155          <FONT color="red">Consider&#x00a0;</FONT>
1156          <xsl:apply-templates select="*[2]"/>
1157         </xsl:otherwise>
1158        </xsl:choose>
1159        <br/>
1160        <xsl:call-template name="make_indent">
1161         <xsl:with-param name="current_indent" select="$current_indent"/>
1162        </xsl:call-template>
1163        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
1164        <xsl:apply-templates select="*[3]"/>
1165        <br/>
1166        <xsl:call-template name="make_indent">
1167         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1168        </xsl:call-template>
1169        <FONT color="red">Left: suppose&#x00a0;</FONT>
1170        <xsl:text>(</xsl:text>
1171        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1172        <xsl:text>)&#x00a0;</xsl:text>
1173        <xsl:apply-templates
1174             select="*[4]/m:bvar/m:type/*[1]"/>
1175        <br/>
1176        <xsl:call-template name="make_indent">
1177         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1178        </xsl:call-template>
1179        <xsl:apply-templates
1180             select="*[4]/*[3]">
1181         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1182        </xsl:apply-templates>
1183        <br/>
1184        <xsl:call-template name="make_indent">
1185         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1186        </xsl:call-template>
1187        <FONT color="red">Right: suppose&#x00a0;</FONT>
1188        <xsl:text>(</xsl:text>
1189        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1190        <xsl:text>)&#x00a0;</xsl:text>
1191        <xsl:apply-templates
1192             select="*[5]/m:bvar/m:type/*[1]"/>
1193        <br/>
1194        <xsl:call-template name="make_indent">
1195         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1196        </xsl:call-template>
1197        <xsl:apply-templates
1198             select="*[5]/*[3]">
1199         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1200        </xsl:apply-templates>
1201       </xsl:when>
1202       <!-- or_ind -->
1203       <xsl:when test="$name='or_ind'">
1204        <xsl:choose>
1205         <xsl:when test="name(*[2])='m:apply'">
1206          <xsl:apply-templates select="*[2]">
1207           <xsl:with-param name="current_indent" select="$current_indent"/>
1208          </xsl:apply-templates>
1209         </xsl:when>
1210         <xsl:otherwise>
1211          <FONT color="red">Consider&#x00a0;</FONT>
1212          <xsl:apply-templates select="*[2]"/>
1213         </xsl:otherwise>
1214        </xsl:choose>
1215        <br/>
1216        <xsl:call-template name="make_indent">
1217         <xsl:with-param name="current_indent" select="$current_indent"/>
1218        </xsl:call-template>
1219        <FONT color="red">We prove&#x00a0;</FONT>
1220        <xsl:apply-templates select="*[3]"/>
1221        <FONT color="red">&#x00a0;by cases:</FONT>
1222        <br/>
1223        <xsl:call-template name="make_indent">
1224         <xsl:with-param name="current_indent" select="$current_indent"/>
1225        </xsl:call-template>
1226        *
1227        <xsl:apply-templates select="*[4]">
1228         <xsl:with-param name="current_indent" select="$current_indent"/>
1229        </xsl:apply-templates>
1230        <br/>
1231        <xsl:call-template name="make_indent">
1232         <xsl:with-param name="current_indent" select="$current_indent"/>
1233        </xsl:call-template>
1234        *
1235        <xsl:apply-templates select="*[5]">
1236         <xsl:with-param name="current_indent" select="$current_indent"/>
1237        </xsl:apply-templates>
1238       </xsl:when>
1239       <!-- Ex_ind -->
1240       <xsl:when test="$name='ex_ind'">
1241        <xsl:choose>
1242         <xsl:when test="name(*[2])='m:apply'">
1243          <xsl:apply-templates select="*[2]">
1244           <xsl:with-param name="current_indent" select="$current_indent"/>
1245          </xsl:apply-templates>
1246         </xsl:when>
1247         <xsl:otherwise>
1248          <FONT color="red">Consider&#x00a0;</FONT>
1249          <xsl:apply-templates select="*[2]">
1250           <xsl:with-param name="current_indent" select="$current_indent"/>
1251          </xsl:apply-templates>
1252         </xsl:otherwise>
1253        </xsl:choose>
1254        <br/>
1255        <xsl:call-template name="make_indent">
1256         <xsl:with-param name="current_indent" select="$current_indent"/>
1257        </xsl:call-template>
1258        <FONT color="red">Let&#x00a0;</FONT>
1259        <xsl:apply-templates mode="inline" select="*[3]"/>
1260        :
1261        <xsl:apply-templates mode="inline" select="*[4]"/>
1262        <FONT color="red">&#x00a0;such that</FONT>
1263        <br/>
1264        <xsl:call-template name="make_indent">
1265         <xsl:with-param name="current_indent" select="$current_indent"/>
1266        </xsl:call-template>
1267        (
1268        <xsl:apply-templates mode="inline" select="*[5]"/>
1269        )
1270        <xsl:apply-templates select="*[6]">
1271         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1272        </xsl:apply-templates>
1273        <br/>
1274        <xsl:call-template name="make_indent">
1275         <xsl:with-param name="current_indent" select="$current_indent"/>
1276        </xsl:call-template>
1277        <xsl:apply-templates select="*[7]">
1278         <xsl:with-param name="current_indent" select="$current_indent"/>
1279        </xsl:apply-templates>
1280       </xsl:when>
1281       <!-- ***************************************** -->
1282       <!-- *********** LAMBDA ELEMENTS ************** -->
1283       <!-- ***************************************** -->
1284       <xsl:when test="$name='subst'">
1285        <xsl:apply-templates select="*[3]"/>
1286        <xsl:text>[</xsl:text>
1287        <xsl:apply-templates select="*[4]"/>
1288        <a href="{*[1]/@definitionURL}">
1289        <FONT color="blue" SIZE="+0" FACE="symbol">
1290         <xsl:text>&#x00ac;</xsl:text>
1291        </FONT>
1292        </a>
1293        <xsl:apply-templates select="*[2]"/>
1294        <xsl:text>]</xsl:text>
1295       </xsl:when>
1296
1297       <xsl:when test="$name='lift_with_base'">
1298        <SUB>
1299        <xsl:apply-templates select="*[3]" mode="inline"/>
1300        </SUB>
1301        <a href="{*[1]/@definitionURL}">
1302        <FONT color="green" FACE="symbol">
1303         <xsl:text>&#x00ad;</xsl:text>
1304        </FONT>
1305        </a>
1306        <SUP>
1307        <xsl:apply-templates select="*[4]" mode="inline"/>
1308        </SUP>
1309        <xsl:text>(</xsl:text>
1310        <xsl:apply-templates select="*[2]" mode="inline"/>
1311        <xsl:text>)</xsl:text>
1312       </xsl:when>
1313
1314       <xsl:when test="$name='lift'">
1315        <a href="{*[1]/@definitionURL}">
1316        <FONT color="green" FACE="symbol">
1317         <xsl:text>&#x00ad;</xsl:text>
1318        </FONT>
1319        </a>
1320        <SUP>
1321        <xsl:apply-templates select="*[2]" mode="inline"/>
1322        </SUP>
1323        <xsl:text>(</xsl:text>
1324        <xsl:apply-templates select="*[3]" mode="inline"/>
1325        <xsl:text>)</xsl:text>
1326       </xsl:when>
1327
1328       <!-- reduction -->
1329       <xsl:when test="$name='beta_red1'">
1330        <xsl:apply-templates select="*[2]" mode="inline"/>
1331        <a href="{*[1]/@definitionURL}">
1332        <FONT color="green" FACE="symbol">
1333         <xsl:text>&#x00ae;</xsl:text>
1334        </FONT>
1335        <SUB>
1336         <FONT color="green" FACE="symbol">
1337          <xsl:text>&#x0062;</xsl:text>
1338         </FONT>
1339        </SUB>
1340        </a>
1341        <xsl:apply-templates select="*[3]" mode="inline"/>
1342       </xsl:when>
1343
1344       <xsl:when test="$name='beta_red'">
1345        <xsl:apply-templates select="*[2]" mode="inline"/>
1346        <a href="{*[1]/@definitionURL}">
1347        <FONT color="green" FACE="symbol">
1348         <xsl:text>&#x00ae;</xsl:text>
1349        </FONT>
1350        <SUB>
1351         <FONT color="green" FACE="symbol">
1352          <xsl:text>&#x0062;*</xsl:text>
1353         </FONT>
1354        </SUB>
1355        </a>
1356        <xsl:apply-templates select="*[3]" mode="inline"/>
1357       </xsl:when>
1358
1359       <xsl:when test="$name='par_beta_red1'">
1360        <xsl:apply-templates select="*[2]" mode="inline"/>
1361        <a href="{*[1]/@definitionURL}">
1362        <FONT color="green" FACE="symbol">
1363         <xsl:text>&#x00de;</xsl:text>
1364        </FONT>
1365        <SUB>
1366         <FONT color="green" FACE="symbol">
1367          <xsl:text>&#x0062;</xsl:text>
1368         </FONT>
1369        </SUB>
1370        </a>
1371        <xsl:apply-templates select="*[3]" mode="inline"/>
1372       </xsl:when>
1373
1374       <xsl:when test="$name='par_beta_red'">
1375        <xsl:apply-templates select="*[2]" mode="inline"/>
1376        <a href="{*[1]/@definitionURL}">
1377        <FONT color="green" FACE="symbol">
1378         <xsl:text>&#x00de;</xsl:text>
1379        </FONT>
1380        <SUB>
1381         <FONT color="green" FACE="symbol">
1382          <xsl:text>&#x0062;*</xsl:text>
1383         </FONT>
1384        </SUB>
1385        </a>
1386        <xsl:apply-templates select="*[3]" mode="inline"/>
1387       </xsl:when>
1388
1389       <!-- forgetful -->
1390       <xsl:when test="$name='forgetful'">
1391        <a href="{*[1]/@definitionURL}">|</a>
1392        <xsl:apply-templates select="*[2]" mode="inline"/>
1393        <a href="{*[1]/@definitionURL}">|</a>
1394       </xsl:when>
1395
1396       <!-- boolean algebra of redexes -->
1397
1398       <!-- isomorphic -->
1399       <xsl:when test="$name='isomorphic'">
1400        <xsl:apply-templates select="*[2]" mode="inline"/>
1401        <a href="{*[1]/@definitionURL}">
1402         <FONT color="green" FACE="symbol">
1403         <xsl:text>&#x0040;</xsl:text>
1404        </FONT>
1405        </a>
1406        <xsl:apply-templates select="*[3]" mode="inline"/>
1407       </xsl:when>
1408
1409       <!-- INTERP -->
1410       <xsl:when test="$name='interp'">
1411          <font color="green">[</font>
1412             <xsl:apply-templates select="*[2]"/>
1413          <font color="green">]</font>
1414       </xsl:when>
1415
1416      </xsl:choose>
1417 </xsl:template>
1418
1419 <!-- LAMBDA -->
1420
1421 <xsl:template match="m:lambda">
1422 <xsl:param name="current_indent" select="0"/>
1423     <xsl:variable name="charlength">
1424      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1425      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1426     </xsl:variable>
1427     <!-- <xsl:value-of select="$charlength"/> -->
1428     <!-- <xsl:value-of select="$current_indent"/> -->
1429      <xsl:choose>
1430      <xsl:when test="$charlength > $framewidth">
1431        <!-- &#x03bb; -->
1432        <xsl:call-template name="mksymbol-1">
1433         <xsl:with-param name="symbol" select="'lambda'"/>
1434         <xsl:with-param name="color" select="'red'"/>
1435         <xsl:with-param name="size" select="'+2'"/>
1436        </xsl:call-template>
1437        <xsl:apply-templates select="m:bvar/m:ci"/>
1438        <xsl:text>:</xsl:text>
1439        <xsl:apply-templates select="m:bvar/m:type">
1440         <xsl:with-param name="current_indent"
1441            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1442        </xsl:apply-templates><br/>
1443        <xsl:call-template name="make_indent">
1444         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1445        </xsl:call-template>
1446        <xsl:text>.</xsl:text>
1447        <xsl:apply-templates select="*[position()=2]">
1448         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1449        </xsl:apply-templates>
1450      </xsl:when>
1451      <xsl:otherwise>
1452       <xsl:apply-templates mode="inline" select="."/>
1453      </xsl:otherwise>
1454      </xsl:choose>
1455 </xsl:template>
1456
1457 <!-- href -->
1458 <xsl:template match="m:ci">
1459  <xsl:choose>
1460   <xsl:when test="boolean(@definitionURL)">
1461    <a href="{@definitionURL}">
1462    <xsl:apply-templates/>
1463    </a>
1464   </xsl:when>
1465   <xsl:otherwise>
1466    <xsl:value-of select="."/>
1467   </xsl:otherwise>
1468  </xsl:choose>
1469 </xsl:template>
1470
1471 <!-- COUNTING -->
1472
1473 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1474 <xsl:param name="incurrent_length" select="0"/>
1475     <xsl:choose>
1476     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1477      <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>
1478      <xsl:choose>
1479      <xsl:when test="string($siblength) = &quot;&quot;">
1480       <xsl:value-of select="$incurrent_length + string-length()"/>
1481      </xsl:when>
1482      <xsl:otherwise>
1483       <xsl:value-of select="number($siblength)"/>
1484      </xsl:otherwise>
1485      </xsl:choose>
1486     </xsl:when>
1487     <xsl:otherwise>
1488      <xsl:value-of select="$incurrent_length + string-length()"/>
1489     </xsl:otherwise>
1490     </xsl:choose>
1491 </xsl:template>
1492
1493 <xsl:template match="*" mode="charcount">
1494  <xsl:param name="incurrent_length" select="0"/>
1495  <xsl:choose>
1496   <xsl:when test="count(child::*) = 0">
1497    <xsl:value-of select="$incurrent_length"/>
1498   </xsl:when>
1499   <xsl:otherwise>
1500     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
1501     <xsl:choose>
1502      <xsl:when test="$framewidth >= number($childlength)">
1503       <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
1504       <xsl:choose>
1505        <xsl:when test="string($siblength) = &quot;&quot;">
1506         <xsl:value-of select="number($childlength)"/>
1507        </xsl:when>
1508        <xsl:otherwise>
1509         <xsl:value-of select="number($siblength)"/>
1510        </xsl:otherwise>
1511       </xsl:choose>
1512      </xsl:when>
1513      <xsl:otherwise>
1514       <xsl:value-of select="number($childlength)"/>
1515      </xsl:otherwise>
1516     </xsl:choose>
1517   </xsl:otherwise>
1518  </xsl:choose>
1519 </xsl:template>
1520
1521
1522 <!--***********************************************************************-->
1523 <!-- OBJECTS                                                               -->
1524 <!--***********************************************************************-->
1525
1526 <!-- DEFINITION -->
1527
1528 <xsl:template match="Definition">
1529 <xsl:param name="current_indent" select="0"/>
1530 <p>
1531 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1532 TYPE =<br/>
1533       <xsl:call-template name="make_indent">
1534        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1535       </xsl:call-template>
1536        <xsl:apply-templates select="type/*[1]">
1537         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1538        </xsl:apply-templates><br/>
1539 BODY =<br/>
1540       <xsl:call-template name="make_indent">
1541        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1542       </xsl:call-template>
1543        <xsl:apply-templates select="body/*[1]">
1544         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1545        </xsl:apply-templates>
1546 </p>
1547 </xsl:template>
1548
1549 <!-- AXIOM -->
1550
1551 <xsl:template match="Axiom">
1552 <xsl:param name="current_indent" select="0"/>
1553 <p>
1554 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1555 TYPE =<br/>
1556       <xsl:call-template name="make_indent">
1557        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1558       </xsl:call-template>
1559 <xsl:apply-templates select="type/*[1]">
1560           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1561        </xsl:apply-templates>
1562 </p>
1563 </xsl:template>
1564
1565 <!-- UNFINISHED PROOF -->
1566
1567 <xsl:template match="CurrentProof">
1568 <xsl:param name="current_indent" select="0"/>
1569 <p>
1570 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1571 THESIS:  <xsl:apply-templates select="type/*[1]">
1572           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1573          </xsl:apply-templates><br/>
1574 CONJECTURES:
1575       <xsl:for-each select="Conjecture">
1576       <br/>
1577       <xsl:call-template name="make_indent">
1578        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1579       </xsl:call-template>
1580       <xsl:value-of select="./@no"/> :
1581       <xsl:apply-templates select="./*[1]">
1582        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
1583       </xsl:apply-templates>
1584       </xsl:for-each>
1585       <br/>
1586 PROOF:
1587       <xsl:apply-templates select="body/*[1]">
1588         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1589       </xsl:apply-templates>
1590 </p>
1591 </xsl:template>
1592
1593 <!-- MUTUAL INDUCTIVE DEFINITION -->
1594
1595 <xsl:template match="InductiveDefinition">
1596 <xsl:param name="current_indent" select="0"/>
1597 <p>
1598      <xsl:for-each select="InductiveType">
1599          <xsl:choose>
1600          <xsl:when test="position() = 1">
1601           <xsl:choose>
1602           <xsl:when test="string(./@inductive) = &quot;true&quot;">
1603           INDUCTIVE DEFINITION
1604           </xsl:when>
1605           <xsl:otherwise>
1606           COINDUCTIVE DEFINITION
1607           </xsl:otherwise>
1608           </xsl:choose>
1609          </xsl:when>
1610          <xsl:otherwise>
1611           AND
1612          </xsl:otherwise>
1613          </xsl:choose>
1614          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
1615          [
1616           <xsl:if test="string(../Param) != &quot;&quot;">
1617            <xsl:for-each select="../Param">
1618             <xsl:value-of select="./@name"/>
1619             :
1620             <xsl:apply-templates select="*"/>
1621            </xsl:for-each>
1622           </xsl:if>
1623          ] <br/>
1624          OF ARITY
1625          <xsl:apply-templates select="./arity/*[1]">
1626           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1627          </xsl:apply-templates> <br/>
1628          BUILT FROM:
1629       <xsl:for-each select="./Constructor">
1630       <br/>
1631       <xsl:call-template name="make_indent">
1632        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1633       </xsl:call-template>
1634          <xsl:choose>
1635          <xsl:when test="position() = 1">
1636          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1637          </xsl:when>
1638          <xsl:otherwise>
1639          <xsl:text>| </xsl:text>
1640          </xsl:otherwise>
1641          </xsl:choose>
1642          <xsl:value-of select="./@name"/>
1643          <xsl:text>: </xsl:text>
1644          <xsl:apply-templates select="./*[1]">
1645           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1646          </xsl:apply-templates>
1647       </xsl:for-each>
1648      </xsl:for-each>
1649 </p>
1650 </xsl:template>
1651
1652 <!-- VARIABLE -->
1653
1654 <xsl:template match="Variable">
1655 <xsl:param name="current_indent" select="0"/>
1656 <p>
1657 VARIABLE <xsl:value-of select="@name"/><br/>
1658 TYPE = <xsl:apply-templates select="type/*[1]">
1659           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1660        </xsl:apply-templates>
1661 </p>
1662 </xsl:template>
1663
1664 <!--***********************************************************************-->
1665 <!-- SECTIONS                                                              -->
1666 <!--***********************************************************************-->
1667
1668 <!-- SECTION -->
1669
1670 <xsl:template match="SECTION">
1671 <xsl:param name="current_indent" select="0"/>
1672  <h1>BEGIN OF SECTION</h1>
1673   <xsl:apply-templates/>
1674  <h1>END OF SECTION</h1>
1675 </xsl:template>
1676
1677 </xsl:stylesheet>