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