helm/style/content_to_html.xsl

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