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                      -->
  33 <!--***********************************************************************-->
  34
  35
  36 <xsl:include href="html_init.xsl"/>
  37 <xsl:include href="html_set.xsl"/>
  38 <xsl:include href="html_reals.xsl"/>
  39
  40 <xsl:variable name="showcast" select="0"/>
  41
  42
  43 <!--***********************************************************************-->
  44 <!-- HTML Head and Body                                                    -->
  45 <!--***********************************************************************-->
  46
  47 <xsl:output method="html"/>
  48
  49 <xsl:variable name="framewidth" select="36"/>
  50
  51 <xsl:template match="/">
  52  <xsl:param name="current_indent" select="0"/>
  53                <html>
  54                 <head></head>
  55                 <body>
  56                 <xsl:apply-templates>
  57                  <xsl:with-param name="current_indent" select="0"/>
  58                 </xsl:apply-templates>
  59                 </body>
  60                </html>
  61 </xsl:template>
  62
  63 <!--***********************************************************************-->
  64 <!-- Indentation                                                           -->
  65 <!--***********************************************************************-->
  66
  67 <xsl:template name="make_indent">
  68  <xsl:param name="current_indent" select="0"/>
  69   <xsl:if test="$current_indent > 0">
  70    <xsl:text>&#x00A0;</xsl:text>
  71    <xsl:call-template name="make_indent">
  72     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
  73    </xsl:call-template>
  74   </xsl:if>
  75 </xsl:template>
  76
  77 <!-- Syntactic Sugar -->
  78
  79 <xsl:template match="m:type">
  80 <xsl:param name="current_indent" select="0"/>
  81 <xsl:apply-templates>
  82  <xsl:with-param name="current_indent"
  83            select="$current_indent"/>
  84 </xsl:apply-templates>
  85 </xsl:template>
  86
  87 <xsl:template match="m:condition">
  88 <xsl:param name="current_indent" select="0"/>
  89 <xsl:apply-templates>
  90  <xsl:with-param name="current_indent"
  91            select="$current_indent"/>
  92 </xsl:apply-templates>
  93 </xsl:template>
  94
  95 <xsl:template match="m:math">
  96 <xsl:param name="current_indent" select="0"/>
  97 <xsl:apply-templates>
  98  <xsl:with-param name="current_indent"
  99            select="$current_indent"/>
 100 </xsl:apply-templates>
 101 </xsl:template>
 102
 103 <!-- CSYMBOL -->
 104
 105 <xsl:template match="m:apply[m:csymbol]">
 106   <xsl:param name="current_indent" select="0"/>
 107   <xsl:param name="width" select="$framewidth"/>
 108   <xsl:variable name="name">
 109    <xsl:value-of select="m:csymbol"/>
 110   </xsl:variable>
 111   <xsl:variable name="charlength">
 112    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 113   </xsl:variable>
 114      <!-- <xsl:value-of select="$current_indent"/> -->
 115      <!-- <xsl:value-of select="$charlength"/> -->
 116      <xsl:choose>
 117       <xsl:when test="$name='prod'">
 118        <xsl:choose>
 119        <xsl:when test="$charlength > $framewidth">
 120          <!-- &#x03a0; -->
 121          <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#80;</FONT>
 122          <xsl:apply-templates select="m:bvar/m:ci"/>
 123          <xsl:text>:</xsl:text>
 124          <xsl:apply-templates select="m:bvar/m:type">
 125           <xsl:with-param name="current_indent"
 126            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 127          </xsl:apply-templates><BR/>
 128          <xsl:call-template name="make_indent">
 129           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 130          </xsl:call-template>
 131          <xsl:text>.</xsl:text>
 132          <xsl:apply-templates select="*[position()=3]">
 133           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 134          </xsl:apply-templates>
 135        </xsl:when>
 136        <xsl:otherwise>
 137         <!-- &#x03a0; -->
 138         <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#80;</FONT>
 139         <xsl:apply-templates select="m:bvar/m:ci"/>
 140         <xsl:text>:</xsl:text>
 141         <xsl:apply-templates select="m:bvar/m:type"/>
 142         <xsl:text>.</xsl:text>
 143         <xsl:apply-templates select="*[position()=3]"/>
 144        </xsl:otherwise>
 145        </xsl:choose>
 146       </xsl:when>
 147       <xsl:when test="$name='arrow'">
 148        <xsl:choose>
 149        <xsl:when test="$charlength > $framewidth">
 150        <xsl:text>(</xsl:text>
 151        <xsl:apply-templates select="*[position()=2]">
 152         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 153        </xsl:apply-templates>
 154        <BR/>
 155        <xsl:call-template name="make_indent">
 156         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 157        </xsl:call-template>
 158        <!-- -> -->
 159        <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#174;</FONT>
 160        <xsl:apply-templates select="*[position()=3]">
 161         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 162        </xsl:apply-templates>
 163        <xsl:text>)</xsl:text>
 164        </xsl:when>
 165        <xsl:otherwise>
 166         <xsl:text>(</xsl:text>
 167         <xsl:apply-templates select="*[position()=2]"/>
 168         <!-- -> -->
 169         <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#174;</FONT>
 170         <xsl:apply-templates select="*[position()=3]"/>
 171         <xsl:text>)</xsl:text>
 172        </xsl:otherwise>
 173        </xsl:choose>
 174       </xsl:when>
 175       <xsl:when test="$name='app'">
 176        <xsl:choose>
 177        <xsl:when test="$charlength  > $framewidth">
 178         <xsl:text>(</xsl:text>
 179         <xsl:apply-templates select="*[position()=2]">
 180          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 181         </xsl:apply-templates>
 182          <xsl:for-each select="*[position()>2]">
 183           <BR/>
 184            <xsl:call-template name="make_indent">
 185             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 186            </xsl:call-template>
 187             <xsl:apply-templates select=".">
 188              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 189             </xsl:apply-templates>
 190          </xsl:for-each>
 191          <xsl:text>)</xsl:text>
 192        </xsl:when>
 193        <xsl:otherwise>
 194         <xsl:text>(</xsl:text>
 195         <xsl:apply-templates select="*[position()=2]"/>
 196         <xsl:for-each select="*[position()>2]">
 197          <xsl:text>&#x00A0;</xsl:text>
 198          <xsl:apply-templates select="."/>
 199         </xsl:for-each>
 200         <xsl:text>)</xsl:text>
 201        </xsl:otherwise>
 202        </xsl:choose>
 203       </xsl:when>
 204       <xsl:when test="$name='cast'">
 205        <xsl:choose>
 206         <xsl:when test="$showcast = 1">
 207          <xsl:choose>
 208           <xsl:when test="$charlength > $framewidth">
 209            <xsl:text>(</xsl:text>
 210            <xsl:apply-templates select="*[position()=2]">
 211             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 212            </xsl:apply-templates><BR/>
 213            <xsl:call-template name="make_indent">
 214             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 215            <xsl:text>:></xsl:text>
 216            <xsl:apply-templates select="*[position()=3]">
 217             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 218            </xsl:apply-templates>
 219            <xsl:text>)</xsl:text>
 220           </xsl:when>
 221           <xsl:otherwise>
 222            <xsl:text>(</xsl:text>
 223            <xsl:apply-templates select="*[position()=2]"/>
 224            <xsl:text>:></xsl:text>
 225            <xsl:apply-templates select="*[position()=3]"/>
 226            <xsl:text>)</xsl:text>
 227           </xsl:otherwise>
 228          </xsl:choose>
 229         </xsl:when>
 230         <xsl:otherwise>
 231          <xsl:apply-templates select="*[position()=2]">
 232           <xsl:with-param name="current_indent" select="$current_indent"/>
 233          </xsl:apply-templates>
 234         </xsl:otherwise>
 235        </xsl:choose>
 236       </xsl:when>
 237       <xsl:when test="$name='Prop'">
 238        <xsl:text>Prop</xsl:text>
 239       </xsl:when>
 240       <xsl:when test="$name='Set'">
 241        <xsl:text>Set</xsl:text>
 242       </xsl:when>
 243       <xsl:when test="$name='Type'">
 244        <xsl:text>Type</xsl:text>
 245       </xsl:when>
 246       <xsl:when test="$name='mutcase'">
 247        <xsl:choose>
 248        <xsl:when test="$charlength > $framewidth">
 249          <xsl:text>&lt;</xsl:text>
 250          <xsl:apply-templates select="*[position()=2]">
 251           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 252          </xsl:apply-templates>
 253          <xsl:text>&gt; </xsl:text>
 254          <xsl:text>CASE </xsl:text>
 255          <xsl:apply-templates select="*[position()=3]">
 256           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 257          </xsl:apply-templates>
 258          <xsl:text> OF </xsl:text>
 259          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 260          <BR/>
 261          <xsl:call-template name="make_indent">
 262             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 263          </xsl:call-template>
 264             <xsl:choose>
 265             <xsl:when test="position() = 1">
 266              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 267             </xsl:when>
 268             <xsl:otherwise>
 269              <xsl:text>| </xsl:text>
 270             </xsl:otherwise>
 271             </xsl:choose>
 272             <xsl:apply-templates select="."/>
 273             <FONT FACE="symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 274             <xsl:apply-templates select="following-sibling::*[position()= 1]">
 275              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
 276             </xsl:apply-templates>
 277          </xsl:for-each>
 278        </xsl:when>
 279        <xsl:otherwise>
 280         <xsl:text>&lt;</xsl:text>
 281         <xsl:apply-templates select="*[position()=2]"/>
 282         <xsl:text>&gt; </xsl:text>
 283         <xsl:text>CASE </xsl:text>
 284         <xsl:apply-templates select="*[position()=3]"/>
 285         <xsl:text> OF </xsl:text>
 286         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 287          <xsl:choose>
 288          <xsl:when test="not(position() = 1)">
 289           <xsl:text> | </xsl:text>
 290          </xsl:when>
 291          </xsl:choose>
 292          <xsl:apply-templates select="."/>
 293          <FONT FACE="symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 294          <xsl:apply-templates select="following-sibling::*[position()= 1]">
 295           <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
 296          </xsl:apply-templates>
 297         </xsl:for-each>
 298        </xsl:otherwise>
 299        </xsl:choose>
 300       </xsl:when>
 301       <xsl:when test="$name='fix'">
 302        <xsl:choose>
 303        <xsl:when test="$charlength  > $framewidth">
 304             <xsl:text>FIX</xsl:text>
 305             <xsl:value-of select="m:ci"/>
 306             <xsl:text>{</xsl:text>
 307             <xsl:for-each select="m:bvar">
 308               <BR/>
 309               <xsl:call-template name="make_indent">
 310                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 311               </xsl:call-template>
 312               <xsl:value-of select="m:ci"/>
 313               <xsl:text>:</xsl:text>
 314               <xsl:apply-templates select="m:type">
 315                <xsl:with-param name="current_indent"
 316                     select="$current_indent + 5 + string-length(m:ci)"/>
 317                </xsl:apply-templates>
 318               <BR/>
 319               <xsl:call-template name="make_indent">
 320                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 321               </xsl:call-template>
 322               <xsl:text>:=</xsl:text>
 323               <xsl:apply-templates select="following-sibling::*[position() = 1]">
 324                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 325               </xsl:apply-templates>
 326             </xsl:for-each>
 327              <BR/>
 328               <xsl:call-template name="make_indent">
 329                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 330               </xsl:call-template>
 331            <xsl:text>}</xsl:text>
 332        </xsl:when>
 333        <xsl:otherwise>
 334         <xsl:text>FIX</xsl:text>
 335         <xsl:value-of select="m:ci"/>
 336         <xsl:text>{</xsl:text>
 337         <xsl:for-each select="m:bvar">
 338             <xsl:value-of select="m:ci"/>
 339             <xsl:text>:</xsl:text>
 340             <xsl:apply-templates select="m:type"/>
 341             <xsl:text>:=</xsl:text>
 342             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 343             <xsl:choose>
 344              <xsl:when test="position()=last()">
 345              <xsl:text>}</xsl:text>
 346              </xsl:when>
 347              <xsl:otherwise>
 348              <xsl:text>;</xsl:text>
 349              </xsl:otherwise>
 350             </xsl:choose>
 351          </xsl:for-each>
 352        </xsl:otherwise>
 353        </xsl:choose>
 354       </xsl:when>
 355       <xsl:when test="$name='cofix'">
 356        <xsl:choose>
 357        <xsl:when test="($charlength + 10) > $framewidth">
 358             <xsl:text>COFIX</xsl:text>
 359             <xsl:value-of select="m:ci"/>
 360             <xsl:text>{</xsl:text>
 361             <BR/>
 362             <xsl:call-template name="make_indent">
 363              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 364             </xsl:call-template>
 365             <xsl:for-each select="m:bvar">
 366                 <xsl:value-of select="m:ci"/>
 367                 <xsl:text>:</xsl:text>
 368                 <xsl:apply-templates select="m:type">
 369                  <xsl:with-param name="current_indent"
 370                     select="$current_indent + 5 + string-length(m:ci)"/>
 371                 </xsl:apply-templates>
 372                 <BR/>
 373                 <xsl:call-template name="make_indent">
 374                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 375                 </xsl:call-template>
 376                 <xsl:text>:=</xsl:text>
 377                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 378                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 379                 </xsl:apply-templates>
 380
 381             </xsl:for-each>
 382             <BR/>
 383               <xsl:call-template name="make_indent">
 384                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 385               </xsl:call-template>
 386             <xsl:text>}</xsl:text>
 387        </xsl:when>
 388        <xsl:otherwise>
 389         <xsl:text>COFIX</xsl:text>
 390         <xsl:value-of select="m:ci"/>
 391         <xsl:text>{</xsl:text>
 392         <xsl:for-each select="m:bvar">
 393             <xsl:value-of select="m:ci"/>
 394             <xsl:text>:</xsl:text>
 395             <xsl:apply-templates select="m:type"/>
 396             <xsl:text>:=</xsl:text>
 397             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 398             <xsl:choose>
 399              <xsl:when test="position()=last()">
 400              <xsl:text>}</xsl:text>
 401              </xsl:when>
 402              <xsl:otherwise>
 403              <xsl:text>;</xsl:text>
 404              </xsl:otherwise>
 405             </xsl:choose>
 406          </xsl:for-each>
 407        </xsl:otherwise>
 408        </xsl:choose>
 409       </xsl:when>
 410       </xsl:choose>
 411     <!--  </m:mrow> -->
 412 </xsl:template>
 413
 414 <!-- LAMBDA -->
 415
 416 <xsl:template match="m:lambda">
 417 <xsl:param name="current_indent" select="0"/>
 418     <xsl:variable name="charlength">
 419      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
 420      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
 421     </xsl:variable>
 422     <!-- <xsl:value-of select="$charlength"/> -->
 423      <xsl:choose>
 424      <xsl:when test="$charlength > $framewidth">
 425        <!-- &#x03bb; -->
 426        <FONT FACE="symbol" SIZE="+2" mathcolor="red">&#108;</FONT>
 427        <xsl:apply-templates select="m:bvar/m:ci"/>
 428        <xsl:text>:</xsl:text>
 429        <xsl:apply-templates select="m:bvar/m:type">
 430         <xsl:with-param name="current_indent"
 431            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 432        </xsl:apply-templates><BR/>
 433        <xsl:call-template name="make_indent">
 434         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 435        </xsl:call-template>
 436        <xsl:text>.</xsl:text>
 437        <xsl:apply-templates select="*[position()=2]">
 438         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 439        </xsl:apply-templates>
 440      </xsl:when>
 441      <xsl:otherwise>
 442       <!-- &#x03bb; -->
 443       <FONT FACE="symbol" SIZE="+2" mathcolor="red">&#108;</FONT>
 444       <xsl:apply-templates select="m:bvar/m:ci"/>
 445       <xsl:text>:</xsl:text>
 446       <xsl:apply-templates select="m:bvar/m:type"/>
 447       <xsl:text>.</xsl:text>
 448       <xsl:apply-templates select="*[position()=2]"/>
 449      </xsl:otherwise>
 450      </xsl:choose>
 451 </xsl:template>
 452
 453 <!-- href -->
 454 <xsl:template match="m:ci">
 455  <xsl:choose>
 456   <xsl:when test="boolean(@definitionURL)">
 457 <!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
 458 <!--   <xsl:variable name="url">
 459     <xsl:value-of select="concat(string($absPath),
 460      @definitionURL)"/>
 461    </xsl:variable>-->
 462    <a>
 463    <xsl:attribute name="href">
 464     <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
 465    </xsl:attribute>
 466    <xsl:apply-templates/>
 467    </a>
 468   </xsl:when>
 469   <xsl:otherwise>
 470    <xsl:value-of select="."/>
 471   </xsl:otherwise>
 472  </xsl:choose>
 473 </xsl:template>
 474
 475 <!-- COUNTING -->
 476
 477 <xsl:template match="m:ci|m:csymbol" mode="charcount">
 478 <xsl:param name="incurrent_length" select="0"/>
 479     <xsl:choose>
 480     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 481      <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>
 482      <xsl:choose>
 483      <xsl:when test="string($siblength) = &quot;&quot;">
 484       <xsl:value-of select="$incurrent_length + string-length()"/>
 485      </xsl:when>
 486      <xsl:otherwise>
 487       <xsl:value-of select="number($siblength)"/>
 488      </xsl:otherwise>
 489      </xsl:choose>
 490     </xsl:when>
 491     <xsl:otherwise>
 492      <xsl:value-of select="$incurrent_length + string-length()"/>
 493     </xsl:otherwise>
 494     </xsl:choose>
 495 </xsl:template>
 496
 497 <xsl:template match="*" mode="charcount">
 498  <xsl:param name="incurrent_length" select="0"/>
 499  <xsl:choose>
 500   <xsl:when test="count(child::*) = 0">
 501    <xsl:value-of select="$incurrent_length"/>
 502   </xsl:when>
 503   <xsl:otherwise>
 504     <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>
 505     <xsl:choose>
 506      <xsl:when test="$framewidth >= number($childlength)">
 507       <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>
 508       <xsl:choose>
 509        <xsl:when test="string($siblength) = &quot;&quot;">
 510         <xsl:value-of select="number($childlength)"/>
 511        </xsl:when>
 512        <xsl:otherwise>
 513         <xsl:value-of select="number($siblength)"/>
 514        </xsl:otherwise>
 515       </xsl:choose>
 516      </xsl:when>
 517      <xsl:otherwise>
 518       <xsl:value-of select="number($childlength)"/>
 519      </xsl:otherwise>
 520     </xsl:choose>
 521   </xsl:otherwise>
 522  </xsl:choose>
 523 </xsl:template>
 524
 525
 526 <!--***********************************************************************-->
 527 <!-- OBJECTS                                                               -->
 528 <!--***********************************************************************-->
 529
 530 <!-- DEFINITION -->
 531
 532 <xsl:template match="Definition">
 533 <xsl:param name="current_indent" select="0"/>
 534 <p>
 535 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
 536 TYPE =<BR/>
 537       <xsl:call-template name="make_indent">
 538        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 539       </xsl:call-template>
 540        <xsl:apply-templates select="type/*[1]">
 541         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 542        </xsl:apply-templates><BR/>
 543 BODY =<BR/>
 544       <xsl:call-template name="make_indent">
 545        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 546       </xsl:call-template>
 547        <xsl:apply-templates select="body/*[1]">
 548         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 549        </xsl:apply-templates>
 550 </p>
 551 </xsl:template>
 552
 553 <!-- AXIOM -->
 554
 555 <xsl:template match="Axiom">
 556 <xsl:param name="current_indent" select="0"/>
 557 <p>
 558 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
 559 TYPE = <xsl:apply-templates select="type/*[1]">
 560           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 561        </xsl:apply-templates>
 562 </p>
 563 </xsl:template>
 564
 565 <!-- UNFINISHED PROOF -->
 566
 567 <xsl:template match="CurrentProof">
 568 <xsl:param name="current_indent" select="0"/>
 569 <p>
 570 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
 571 THESIS:  <xsl:apply-templates select="type/*[1]">
 572           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 573          </xsl:apply-templates><BR/>
 574 CONJECTURES:
 575       <xsl:for-each select="Conjecture">
 576       <BR/>
 577       <xsl:call-template name="make_indent">
 578        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 579       </xsl:call-template>
 580       <xsl:value-of select="./@no"/> :
 581       <xsl:apply-templates select="./*[1]">
 582        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
 583       </xsl:apply-templates>
 584       </xsl:for-each>
 585       <BR/>
 586 PROOF:
 587       <xsl:apply-templates select="body/*[1]">
 588         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 589       </xsl:apply-templates>
 590 </p>
 591 </xsl:template>
 592
 593 <!-- MUTUAL INDUCTIVE DEFINITION -->
 594
 595 <xsl:template match="InductiveDefinition">
 596 <xsl:param name="current_indent" select="0"/>
 597 <p>
 598      <xsl:for-each select="InductiveType">
 599          <xsl:choose>
 600          <xsl:when test="position() = 1">
 601           <xsl:choose>
 602           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 603           INDUCTIVE DEFINITION
 604           </xsl:when>
 605           <xsl:otherwise>
 606           COINDUCTIVE DEFINITION
 607           </xsl:otherwise>
 608           </xsl:choose>
 609          </xsl:when>
 610          <xsl:otherwise>
 611           AND
 612          </xsl:otherwise>
 613          </xsl:choose>
 614          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
 615          [
 616           <xsl:if test="string(../Param) != &quot;&quot;">
 617            <xsl:for-each select="../Param">
 618             <xsl:value-of select="./@name"/>
 619             :
 620             <xsl:apply-templates select="*"/>
 621            </xsl:for-each>
 622           </xsl:if>
 623          ] <BR/>
 624          OF ARITY
 625          <xsl:apply-templates select="./arity/*[1]">
 626           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 627          </xsl:apply-templates> <BR/>
 628          BUILT FROM:
 629       <xsl:for-each select="./Constructor">
 630       <BR/>
 631       <xsl:call-template name="make_indent">
 632        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 633       </xsl:call-template>
 634          <xsl:choose>
 635          <xsl:when test="position() = 1">
 636          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 637          </xsl:when>
 638          <xsl:otherwise>
 639          <xsl:text>| </xsl:text>
 640          </xsl:otherwise>
 641          </xsl:choose>
 642          <xsl:value-of select="./@name"/>
 643          <xsl:text>: </xsl:text>
 644          <xsl:apply-templates select="./*[1]">
 645           <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
 646          </xsl:apply-templates>
 647       </xsl:for-each>
 648      </xsl:for-each>
 649 </p>
 650 </xsl:template>
 651
 652 <!-- VARIABLE -->
 653
 654 <xsl:template match="Variable">
 655 <xsl:param name="current_indent" select="0"/>
 656 <p>
 657 VARIABLE <xsl:value-of select="@name"/><BR/>
 658 TYPE = <xsl:apply-templates select="type/*[1]">
 659           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 660        </xsl:apply-templates>
 661 </p>
 662 </xsl:template>
 663
 664 <!--***********************************************************************-->
 665 <!-- SECTIONS                                                              -->
 666 <!--***********************************************************************-->
 667
 668 <!-- SECTION -->
 669
 670 <xsl:template match="SECTION">
 671 <xsl:param name="current_indent" select="0"/>
 672  <h1>BEGIN OF SECTION</h1>
 673   <xsl:apply-templates/>
 674  <h1>END OF SECTION</h1>
 675 </xsl:template>
 676
 677 </xsl:stylesheet>