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 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
  36 <xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
  37
  38 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
  39
  40 <xsl:variable name="header"><xsl:value-of select="$processorURL"/>/apply?key=C1&#x26;key=HC2&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
  41
  42 <xsl:include href="html_init.xsl"/>
  43 <xsl:include href="html_set.xsl"/>
  44 <xsl:include href="html_reals.xsl"/>
  45
  46 <xsl:variable name="showcast" select="0"/>
  47
  48
  49 <!--***********************************************************************-->
  50 <!-- HTML Head and Body                                                    -->
  51 <!--***********************************************************************-->
  52
  53 <!-- <xsl:output method="html"/> -->
  54 <xsl:output method="html" encoding="iso-8859-1"/>
  55
  56 <xsl:variable name="framewidth" select="36"/>
  57
  58 <xsl:template match="/">
  59  <xsl:param name="current_indent" select="0"/>
  60                <html>
  61                 <head>
  62                  <style>
  63                  A { text-decoration: none }
  64                  </style>
  65                 </head>
  66                 <body bgcolor="white">
  67                 <xsl:apply-templates>
  68                  <xsl:with-param name="current_indent" select="0"/>
  69                 </xsl:apply-templates>
  70                 </body>
  71                </html>
  72 </xsl:template>
  73
  74 <!--***********************************************************************-->
  75 <!-- Indentation                                                           -->
  76 <!--***********************************************************************-->
  77
  78 <xsl:template name="make_indent">
  79  <xsl:param name="current_indent" select="0"/>
  80   <xsl:if test="$current_indent > 0">
  81    <xsl:text>&#x00a0;</xsl:text>
  82    <xsl:call-template name="make_indent">
  83     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
  84    </xsl:call-template>
  85   </xsl:if>
  86 </xsl:template>
  87
  88 <!-- Syntactic Sugar -->
  89 <xsl:template match="m:type">
  90 <xsl:param name="current_indent" select="0"/>
  91 <xsl:apply-templates>
  92  <xsl:with-param name="current_indent"
  93            select="$current_indent"/>
  94 </xsl:apply-templates>
  95 </xsl:template>
  96
  97 <xsl:template match="m:condition">
  98 <xsl:param name="current_indent" select="0"/>
  99 <xsl:apply-templates>
 100  <xsl:with-param name="current_indent"
 101            select="$current_indent"/>
 102 </xsl:apply-templates>
 103 </xsl:template>
 104
 105 <xsl:template match="m:math">
 106 <xsl:param name="current_indent" select="0"/>
 107 <xsl:apply-templates>
 108  <xsl:with-param name="current_indent"
 109            select="$current_indent"/>
 110 </xsl:apply-templates>
 111 </xsl:template>
 112
 113 <!--*********************************************************************-->
 114 <!--                         INLINE MODE                                 -->
 115 <!--*********************************************************************-->
 116
 117 <!-- href -->
 118 <xsl:template mode="inline" match="m:ci">
 119  <xsl:choose>
 120   <xsl:when test="boolean(@definitionURL)">
 121    <a>
 122    <xsl:attribute name="href">
 123     <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
 124    </xsl:attribute>
 125    <xsl:apply-templates/>
 126    </a>
 127   </xsl:when>
 128   <xsl:otherwise>
 129    <xsl:value-of select="."/>
 130   </xsl:otherwise>
 131  </xsl:choose>
 132 </xsl:template>
 133
 134 <!-- CSYMBOL -->
 135
 136 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 137    <xsl:variable name="name">
 138     <xsl:value-of select="m:csymbol"/>
 139    </xsl:variable>
 140    <xsl:choose>
 141     <!-- FORALL -->
 142     <xsl:when test="$name='forall'">
 143      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 144      <xsl:apply-templates select="m:bvar/m:ci"/>
 145      <xsl:text>:</xsl:text>
 146      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 147      <xsl:text>.</xsl:text>
 148      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 149     </xsl:when>
 150     <xsl:when test="$name='prod'">
 151      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 152      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 153      <xsl:text>:</xsl:text>
 154      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 155      <xsl:text>.</xsl:text>
 156      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 157     </xsl:when>
 158     <!-- ARROW -->
 159     <xsl:when test="$name='arrow'">
 160      <xsl:text>(</xsl:text>
 161      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 162      <FONT color="blue" FACE="symbol">
 163       <xsl:text>&#x00ae;</xsl:text>
 164      </FONT>
 165      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 166      <xsl:text>)</xsl:text>
 167     </xsl:when>
 168     <!-- APP -->
 169     <xsl:when test="$name='app'">
 170      <xsl:text>(</xsl:text>
 171      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 172      <xsl:for-each select="*[position()>2]">
 173       <xsl:text>&#x00A0;</xsl:text>
 174       <xsl:apply-templates mode="inline" select="."/>
 175      </xsl:for-each>
 176      <xsl:text>)</xsl:text>
 177     </xsl:when>
 178     <!-- CAST -->
 179     <xsl:when test="$name='cast'">
 180      <xsl:text>(</xsl:text>
 181      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 182      <xsl:text>:></xsl:text>
 183      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 184      <xsl:text>)</xsl:text>
 185     </xsl:when>
 186     <xsl:when test="$name='Prop'">
 187      <FONT color="violet">Prop</FONT>
 188     </xsl:when>
 189     <xsl:when test="$name='Set'">
 190      <FONT color="violet">Set</FONT>
 191     </xsl:when>
 192     <xsl:when test="$name='Type'">
 193      <FONT color="violet">Type</FONT>
 194     </xsl:when>
 195     <!-- MUTCASE -->
 196     <xsl:when test="$name='mutcase'">
 197      <xsl:text>&lt;</xsl:text>
 198      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 199      <xsl:text>&gt; </xsl:text>
 200      <FONT color="red">CASE </FONT>
 201      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 202      <FONT color="red"> OF </FONT>
 203      <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 204       <xsl:choose>
 205        <xsl:when test="not(position() = 1)">
 206         <xsl:text> | </xsl:text>
 207        </xsl:when>
 208       </xsl:choose>
 209       <xsl:apply-templates mode="inline" select="."/>
 210       <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 211       <xsl:apply-templates mode="inline"
 212            select="following-sibling::*[position()= 1]"/>
 213      </xsl:for-each>
 214     </xsl:when>
 215     <!-- FIX -->
 216     <xsl:when test="$name='fix'">
 217      <FONT color="red">FIX</FONT>
 218      <xsl:value-of select="m:ci"/>
 219      <xsl:text>{</xsl:text>
 220      <xsl:for-each select="m:bvar">
 221       <xsl:value-of select="m:ci"/>
 222       <xsl:text>:</xsl:text>
 223       <xsl:apply-templates mode="inline" select="m:type"/>
 224       <xsl:text>:=</xsl:text>
 225       <xsl:apply-templates mode="inline"
 226              select="following-sibling::*[position() = 1]"/>
 227       <xsl:choose>
 228        <xsl:when test="position()=last()">
 229         <xsl:text>}</xsl:text>
 230        </xsl:when>
 231        <xsl:otherwise>
 232         <xsl:text>;</xsl:text>
 233        </xsl:otherwise>
 234       </xsl:choose>
 235      </xsl:for-each>
 236     </xsl:when>
 237     <!-- COFIX -->
 238     <xsl:when test="$name='cofix'">
 239      <xsl:text>COFIX</xsl:text>
 240      <xsl:value-of select="m:ci"/>
 241      <xsl:text>{</xsl:text>
 242      <xsl:for-each select="m:bvar">
 243       <xsl:value-of select="m:ci"/>
 244       <xsl:text>:</xsl:text>
 245       <xsl:apply-templates mode="inline" select="m:type"/>
 246       <xsl:text>:=</xsl:text>
 247       <xsl:apply-templates mode="inline"
 248           select="following-sibling::*[position() = 1]"/>
 249       <xsl:choose>
 250        <xsl:when test="position()=last()">
 251         <xsl:text>}</xsl:text>
 252        </xsl:when>
 253        <xsl:otherwise>
 254         <xsl:text>;</xsl:text>
 255        </xsl:otherwise>
 256       </xsl:choose>
 257      </xsl:for-each>
 258     </xsl:when>
 259     <!-- proof -->
 260     <xsl:when test="$name='proof'">
 261        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 262        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 263        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 264     </xsl:when>
 265     <!-- and_ind -->
 266     <xsl:when test="$name='and_ind'">
 267      <FONT color="red">From&#x00a0;</FONT>
 268      <xsl:apply-templates select="*[2]"/>
 269      <FONT color="red">&#x00a0;we get</FONT>
 270      <m:mtext>(</m:mtext>
 271      <xsl:apply-templates select="*[3]"/>
 272      <m:mtext>)&#x00a0;</m:mtext>
 273      <xsl:apply-templates mode="inline" select="*[4]"/>
 274      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 275      <m:mtext>(</m:mtext>
 276      <xsl:apply-templates select="*[5]"/>
 277      <m:mtext>)&#x00a0;</m:mtext>
 278      <xsl:apply-templates mode="inline" select="*[6]"/>
 279      <m:mtext>;</m:mtext>
 280      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 281      <xsl:apply-templates mode="inline" select="*[7]"/>
 282     </xsl:when>
 283    </xsl:choose>
 284 </xsl:template>
 285
 286 <xsl:template mode="inline" match="m:lambda">
 287       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
 288       <xsl:apply-templates select="m:bvar/m:ci"/>
 289       <xsl:text>:</xsl:text>
 290       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 291       <xsl:text>.</xsl:text>
 292       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 293 </xsl:template>
 294
 295 <!--*********************************************************************-->
 296 <!--                       COUNTING MODE                                 -->
 297 <!--*********************************************************************-->
 298
 299 <xsl:template match="m:apply[m:csymbol]">
 300   <xsl:param name="current_indent" select="0"/>
 301   <xsl:param name="width" select="$framewidth"/>
 302   <xsl:variable name="name">
 303    <xsl:value-of select="m:csymbol"/>
 304   </xsl:variable>
 305   <xsl:variable name="charlength">
 306    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 307   </xsl:variable>
 308      <!-- <xsl:value-of select="$current_indent"/> -->
 309      <!-- <xsl:value-of select="$charlength"/> -->
 310      <xsl:choose>
 311      <!-- FORALL -->
 312       <xsl:when test="$name='forall'">
 313        <xsl:choose>
 314        <xsl:when test="$charlength > $framewidth">
 315          <!-- &#x03a0; -->
 316          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 317          <xsl:apply-templates select="m:bvar/m:ci"/>
 318          <xsl:text>:</xsl:text>
 319          <xsl:apply-templates select="m:bvar/m:type">
 320           <xsl:with-param name="current_indent"
 321            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 322          </xsl:apply-templates>
 323          <br/>
 324          <xsl:call-template name="make_indent">
 325           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 326          </xsl:call-template>
 327          <xsl:text>.</xsl:text>
 328          <xsl:apply-templates select="*[position()=3]">
 329           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 330          </xsl:apply-templates>
 331        </xsl:when>
 332        <xsl:otherwise>
 333         <xsl:apply-templates mode="inline" select="."/>
 334        </xsl:otherwise>
 335        </xsl:choose>
 336       </xsl:when>
 337       <!-- PROD -->
 338       <xsl:when test="$name='prod'">
 339        <xsl:choose>
 340        <xsl:when test="$charlength > $framewidth">
 341          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 342          <xsl:apply-templates select="m:bvar/m:ci"/>
 343          <xsl:text>:</xsl:text>
 344          <xsl:apply-templates select="m:bvar/m:type">
 345           <xsl:with-param name="current_indent"
 346            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 347          </xsl:apply-templates><br/>
 348          <xsl:call-template name="make_indent">
 349           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 350          </xsl:call-template>
 351          <xsl:text>.</xsl:text>
 352          <xsl:apply-templates select="*[position()=3]">
 353           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 354          </xsl:apply-templates>
 355        </xsl:when>
 356        <xsl:otherwise>
 357         <xsl:apply-templates mode="inline" select="."/>
 358        </xsl:otherwise>
 359        </xsl:choose>
 360       </xsl:when>
 361       <!-- ARROW -->
 362       <xsl:when test="$name='arrow'">
 363        <xsl:choose>
 364        <xsl:when test="$charlength > $framewidth">
 365        <xsl:text>(</xsl:text>
 366        <xsl:apply-templates select="*[position()=2]">
 367         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 368        </xsl:apply-templates>
 369        <br/>
 370        <xsl:call-template name="make_indent">
 371         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 372        </xsl:call-template>
 373        <!-- -> -->
 374        <FONT color="blue" FACE="symbol">
 375         <xsl:text>&#x00ae;</xsl:text>
 376        </FONT>
 377        <xsl:apply-templates select="*[position()=3]">
 378         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 379        </xsl:apply-templates>
 380        <xsl:text>)</xsl:text>
 381        </xsl:when>
 382        <xsl:otherwise>
 383         <xsl:apply-templates mode="inline" select="."/>
 384        </xsl:otherwise>
 385        </xsl:choose>
 386       </xsl:when>
 387       <!-- APP -->
 388       <xsl:when test="$name='app'">
 389        <xsl:choose>
 390        <xsl:when test="$charlength  > $framewidth">
 391         <xsl:text>(</xsl:text>
 392         <xsl:apply-templates select="*[position()=2]">
 393          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 394         </xsl:apply-templates>
 395          <xsl:for-each select="*[position()>2]">
 396           <br/>
 397            <xsl:call-template name="make_indent">
 398             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 399            </xsl:call-template>
 400             <xsl:apply-templates select=".">
 401              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 402             </xsl:apply-templates>
 403          </xsl:for-each>
 404          <xsl:text>)</xsl:text>
 405        </xsl:when>
 406        <xsl:otherwise>
 407         <xsl:apply-templates mode="inline" select="."/>
 408        </xsl:otherwise>
 409        </xsl:choose>
 410       </xsl:when>
 411       <xsl:when test="$name='cast'">
 412        <xsl:choose>
 413         <xsl:when test="$showcast = 1">
 414          <xsl:choose>
 415           <xsl:when test="$charlength > $framewidth">
 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><br/>
 420            <xsl:call-template name="make_indent">
 421             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 422            <xsl:text>:></xsl:text>
 423            <xsl:apply-templates select="*[position()=3]">
 424             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 425            </xsl:apply-templates>
 426            <xsl:text>)</xsl:text>
 427           </xsl:when>
 428           <xsl:otherwise>
 429            <xsl:apply-templates mode="inline" select="."/>
 430           </xsl:otherwise>
 431          </xsl:choose>
 432         </xsl:when>
 433         <xsl:otherwise>
 434          <xsl:apply-templates select="*[position()=2]">
 435           <xsl:with-param name="current_indent" select="$current_indent"/>
 436          </xsl:apply-templates>
 437         </xsl:otherwise>
 438        </xsl:choose>
 439       </xsl:when>
 440       <xsl:when test="$name='Prop'">
 441        <xsl:text>Prop</xsl:text>
 442       </xsl:when>
 443       <xsl:when test="$name='Set'">
 444        <xsl:text>Set</xsl:text>
 445       </xsl:when>
 446       <xsl:when test="$name='Type'">
 447        <xsl:text>Type</xsl:text>
 448       </xsl:when>
 449       <xsl:when test="$name='mutcase'">
 450        <xsl:choose>
 451        <xsl:when test="$charlength > $framewidth">
 452          <xsl:text>&lt;</xsl:text>
 453          <xsl:apply-templates select="*[position()=2]">
 454           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 455          </xsl:apply-templates>
 456          <xsl:text>&gt; </xsl:text>
 457          <xsl:text>CASE </xsl:text>
 458          <xsl:apply-templates select="*[position()=3]">
 459           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 460          </xsl:apply-templates>
 461          <xsl:text> OF </xsl:text>
 462          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 463          <br/>
 464          <xsl:call-template name="make_indent">
 465             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 466          </xsl:call-template>
 467             <xsl:choose>
 468             <xsl:when test="position() = 1">
 469              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 470             </xsl:when>
 471             <xsl:otherwise>
 472              <xsl:text>| </xsl:text>
 473             </xsl:otherwise>
 474             </xsl:choose>
 475             <xsl:apply-templates select="."/>
 476             <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
 477             <xsl:apply-templates select="following-sibling::*[position()= 1]">
 478              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
 479             </xsl:apply-templates>
 480          </xsl:for-each>
 481        </xsl:when>
 482        <xsl:otherwise>
 483         <xsl:apply-templates mode="inline" select="."/>
 484        </xsl:otherwise>
 485        </xsl:choose>
 486       </xsl:when>
 487       <!-- FIX -->
 488       <xsl:when test="$name='fix'">
 489        <xsl:choose>
 490        <xsl:when test="$charlength  > $framewidth">
 491             <xsl:text>FIX</xsl:text>
 492             <xsl:value-of select="m:ci"/>
 493             <xsl:text>{</xsl:text>
 494             <xsl:for-each select="m:bvar">
 495               <br/>
 496               <xsl:call-template name="make_indent">
 497                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 498               </xsl:call-template>
 499               <xsl:value-of select="m:ci"/>
 500               <xsl:text>:</xsl:text>
 501               <xsl:apply-templates select="m:type">
 502                <xsl:with-param name="current_indent"
 503                     select="$current_indent + 5 + string-length(m:ci)"/>
 504                </xsl:apply-templates>
 505               <br/>
 506               <xsl:call-template name="make_indent">
 507                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 508               </xsl:call-template>
 509               <xsl:text>:=</xsl:text>
 510               <xsl:apply-templates select="following-sibling::*[position() = 1]">
 511                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 512               </xsl:apply-templates>
 513             </xsl:for-each>
 514              <br/>
 515               <xsl:call-template name="make_indent">
 516                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 517               </xsl:call-template>
 518            <xsl:text>}</xsl:text>
 519        </xsl:when>
 520        <xsl:otherwise>
 521         <xsl:apply-templates mode="inline" select="."/>
 522        </xsl:otherwise>
 523        </xsl:choose>
 524       </xsl:when>
 525       <!-- COFIX -->
 526       <xsl:when test="$name='cofix'">
 527        <xsl:choose>
 528        <xsl:when test="($charlength + 10) > $framewidth">
 529             <xsl:text>COFIX</xsl:text>
 530             <xsl:value-of select="m:ci"/>
 531             <xsl:text>{</xsl:text>
 532             <br/>
 533             <xsl:call-template name="make_indent">
 534              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 535             </xsl:call-template>
 536             <xsl:for-each select="m:bvar">
 537                 <xsl:value-of select="m:ci"/>
 538                 <xsl:text>:</xsl:text>
 539                 <xsl:apply-templates select="m:type">
 540                  <xsl:with-param name="current_indent"
 541                     select="$current_indent + 5 + string-length(m:ci)"/>
 542                 </xsl:apply-templates>
 543                 <br/>
 544                 <xsl:call-template name="make_indent">
 545                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 546                 </xsl:call-template>
 547                 <xsl:text>:=</xsl:text>
 548                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 549                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 550                 </xsl:apply-templates>
 551
 552             </xsl:for-each>
 553             <br/>
 554               <xsl:call-template name="make_indent">
 555                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 556               </xsl:call-template>
 557             <xsl:text>}</xsl:text>
 558        </xsl:when>
 559        <xsl:otherwise>
 560         <xsl:apply-templates mode="inline" select="m:type"/>
 561        </xsl:otherwise>
 562        </xsl:choose>
 563       </xsl:when>
 564       <!-- ***************************************** -->
 565       <!-- *********** PROOF ELEMENTS ************** -->
 566       <!-- ***************************************** -->
 567       <!-- PROOF -->
 568       <xsl:when test="$name='proof'">
 569        <xsl:apply-templates select="*[position()=2]">
 570         <xsl:with-param name="current_indent" select="$current_indent"/>
 571        </xsl:apply-templates>
 572        <br/>
 573        <!-- <xsl:element name="br"/> -->
 574        <xsl:call-template name="make_indent">
 575         <xsl:with-param name="current_indent" select="$current_indent"/>
 576        </xsl:call-template>
 577        <FONT color="red">we proved&#x00a0;</FONT>
 578        <xsl:apply-templates select="*[position()=3]">
 579         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 580        </xsl:apply-templates>
 581       </xsl:when>
 582       <!-- letin1 -->
 583       <xsl:when test="$name='letin1'">
 584        <xsl:apply-templates select="*[position()=2]">
 585         <xsl:with-param name="current_indent" select="$current_indent"/>
 586        </xsl:apply-templates>
 587        <br/>
 588        <xsl:call-template name="make_indent">
 589         <xsl:with-param name="current_indent" select="$current_indent"/>
 590        </xsl:call-template>
 591        <xsl:apply-templates select="*[position()=3]">
 592         <xsl:with-param name="current_indent" select="$current_indent"/>
 593        </xsl:apply-templates>
 594       </xsl:when>
 595       <!-- letin -->
 596       <xsl:when test="$name='letin'">
 597        <xsl:for-each select="*[position()>1 and last()>position()]">
 598         <xsl:apply-templates select=".">
 599          <xsl:with-param name="current_indent" select="$current_indent"/>
 600         </xsl:apply-templates>
 601         <br/>
 602         <xsl:call-template name="make_indent">
 603          <xsl:with-param name="current_indent" select="$current_indent"/>
 604         </xsl:call-template>
 605        </xsl:for-each>
 606        <xsl:apply-templates select="*[position()=last()]">
 607         <xsl:with-param name="current_indent" select="$current_indent"/>
 608        </xsl:apply-templates>
 609       </xsl:when>
 610       <!-- Let -->
 611       <xsl:when test="$name='let'">
 612        <m:mtext>(</m:mtext>
 613        <xsl:apply-templates select="m:ci"/>
 614        <m:mtext>) </m:mtext>
 615        <xsl:apply-templates select="*[3]">
 616         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 617        </xsl:apply-templates>
 618       </xsl:when>
 619       <!-- rw_step -->
 620       <xsl:when test="$name='rw_step'">
 621        <xsl:choose>
 622         <xsl:when test="name(*[2])='m:apply'">
 623          <xsl:apply-templates select="*[2]">
 624           <xsl:with-param name="current_indent" select="$current_indent"/>
 625          </xsl:apply-templates>
 626         </xsl:when>
 627         <xsl:otherwise>
 628          <FONT color="red">Consider&#x00a0;</FONT>
 629          <xsl:apply-templates select="*[2]"/>
 630         </xsl:otherwise>
 631        </xsl:choose>
 632        <br/>
 633        <xsl:call-template name="make_indent">
 634         <xsl:with-param name="current_indent" select="$current_indent"/>
 635        </xsl:call-template>
 636        <FONT color="red">Rewrite&#x00a0;</FONT>
 637        <xsl:apply-templates select="*[3]"/>
 638        <FONT color="red">&#x00a0;with&#x00a0;</FONT>
 639        <xsl:apply-templates select="*[4]"/>
 640        <FONT color="red">&#x00a0;by&#x00a0;</FONT>
 641        <xsl:apply-templates select="*[5]"/>
 642       </xsl:when>
 643       <!-- rewrite and apply -->
 644       <xsl:when test="$name='rewrite_and_apply'">
 645        <xsl:apply-templates select="*[2]">
 646         <xsl:with-param name="current_indent" select="$current_indent"/>
 647        </xsl:apply-templates>
 648        <br/>
 649        <xsl:call-template name="make_indent">
 650         <xsl:with-param name="current_indent" select="$current_indent"/>
 651        </xsl:call-template>
 652        <FONT color="red">Then apply it to&#x00a0;</FONT>
 653        <xsl:apply-templates select="*[position()>2]"/>
 654       </xsl:when>
 655       <!-- and_ind -->
 656       <xsl:when test="$name='and_ind'">
 657        <xsl:choose>
 658         <xsl:when test="name(*[2])='m:apply'">
 659          <xsl:apply-templates select="*[2]">
 660           <xsl:with-param name="current_indent" select="$current_indent"/>
 661          </xsl:apply-templates>
 662         </xsl:when>
 663         <xsl:otherwise>
 664          <FONT color="red">Consider&#x00a0;</FONT>
 665          <xsl:apply-templates select="*[2]"/>
 666         </xsl:otherwise>
 667        </xsl:choose>
 668        <br/>
 669        <xsl:call-template name="make_indent">
 670         <xsl:with-param name="current_indent" select="$current_indent"/>
 671        </xsl:call-template>
 672        <FONT color="red">In particular, we have</FONT>
 673        <br/>
 674        <xsl:call-template name="make_indent">
 675         <xsl:with-param name="current_indent" select="$current_indent"/>
 676        </xsl:call-template>
 677        <m:mtext>(</m:mtext>
 678        <xsl:apply-templates select="*[3]"/>
 679        <m:mtext>)&#x00a0;</m:mtext>
 680        <xsl:apply-templates select="*[4]">
 681         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 682        </xsl:apply-templates>
 683        <br/>
 684        <xsl:call-template name="make_indent">
 685         <xsl:with-param name="current_indent" select="$current_indent"/>
 686        </xsl:call-template>
 687        <m:mtext>(</m:mtext>
 688        <xsl:apply-templates select="*[5]"/>
 689        <m:mtext>)&#x00a0;</m:mtext>
 690        <xsl:apply-templates select="*[6]">
 691         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 692        </xsl:apply-templates>
 693        <br/>
 694        <xsl:call-template name="make_indent">
 695         <xsl:with-param name="current_indent" select="$current_indent"/>
 696        </xsl:call-template>
 697        <xsl:apply-templates select="*[7]">
 698         <xsl:with-param name="current_indent" select="$current_indent"/>
 699        </xsl:apply-templates>
 700       </xsl:when>
 701       <!-- or_ind -->
 702       <xsl:when test="$name='or_ind'">
 703        <xsl:choose>
 704         <xsl:when test="name(*[2])='m:apply'">
 705          <xsl:apply-templates select="*[2]">
 706           <xsl:with-param name="current_indent" select="$current_indent"/>
 707          </xsl:apply-templates>
 708         </xsl:when>
 709         <xsl:otherwise>
 710          <FONT color="red">Consider&#x00a0;</FONT>
 711          <xsl:apply-templates select="*[2]"/>
 712         </xsl:otherwise>
 713        </xsl:choose>
 714        <br/>
 715        <xsl:call-template name="make_indent">
 716         <xsl:with-param name="current_indent" select="$current_indent"/>
 717        </xsl:call-template>
 718        <FONT color="red">We prove&#x00a0;</FONT>
 719        <xsl:apply-templates select="*[3]"/>
 720        <FONT color="red">&#x00a0;by cases:</FONT>
 721        <br/>
 722        <xsl:call-template name="make_indent">
 723         <xsl:with-param name="current_indent" select="$current_indent"/>
 724        </xsl:call-template>
 725        <m:mtext>*</m:mtext>
 726        <xsl:apply-templates select="*[4]">
 727         <xsl:with-param name="current_indent" select="$current_indent"/>
 728        </xsl:apply-templates>
 729        <br/>
 730        <xsl:call-template name="make_indent">
 731         <xsl:with-param name="current_indent" select="$current_indent"/>
 732        </xsl:call-template>
 733        <m:mtext>*</m:mtext>
 734        <xsl:apply-templates select="*[5]">
 735         <xsl:with-param name="current_indent" select="$current_indent"/>
 736        </xsl:apply-templates>
 737       </xsl:when>
 738       <!-- Ex_ind -->
 739       <xsl:when test="$name='ex_ind'">
 740        <xsl:choose>
 741         <xsl:when test="name(*[2])='m:apply'">
 742          <xsl:apply-templates select="*[2]">
 743           <xsl:with-param name="current_indent" select="$current_indent"/>
 744          </xsl:apply-templates>
 745         </xsl:when>
 746         <xsl:otherwise>
 747          <FONT color="red">Consider&#x00a0;</FONT>
 748          <xsl:apply-templates select="*[2]">
 749           <xsl:with-param name="current_indent" select="$current_indent"/>
 750          </xsl:apply-templates>
 751         </xsl:otherwise>
 752        </xsl:choose>
 753        <br/>
 754        <xsl:call-template name="make_indent">
 755         <xsl:with-param name="current_indent" select="$current_indent"/>
 756        </xsl:call-template>
 757        <FONT color="red">Let&#x00a0;</FONT>
 758        <xsl:apply-templates mode="inline" select="*[3]"/>
 759        <m:mtext>:</m:mtext>
 760        <xsl:apply-templates mode="inline" select="*[4]"/>
 761        <FONT color="red">&#x00a0;such that</FONT>
 762        <br/>
 763        <xsl:call-template name="make_indent">
 764         <xsl:with-param name="current_indent" select="$current_indent"/>
 765        </xsl:call-template>
 766        <m:mtext>(</m:mtext>
 767        <xsl:apply-templates mode="inline" select="*[5]"/>
 768        <m:mtext>)</m:mtext>
 769        <xsl:apply-templates select="*[6]">
 770         <xsl:with-param name="current_indent" select="$current_indent +7"/>
 771        </xsl:apply-templates>
 772        <br/>
 773        <xsl:call-template name="make_indent">
 774         <xsl:with-param name="current_indent" select="$current_indent"/>
 775        </xsl:call-template>
 776        <xsl:apply-templates select="*[7]">
 777         <xsl:with-param name="current_indent" select="$current_indent"/>
 778        </xsl:apply-templates>
 779       </xsl:when>
 780      </xsl:choose>
 781 </xsl:template>
 782
 783 <!-- LAMBDA -->
 784
 785 <xsl:template match="m:lambda">
 786 <xsl:param name="current_indent" select="0"/>
 787     <xsl:variable name="charlength">
 788      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
 789      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
 790     </xsl:variable>
 791     <!-- <xsl:value-of select="$charlength"/> -->
 792     <!-- <xsl:value-of select="$current_indent"/> -->
 793      <xsl:choose>
 794      <xsl:when test="$charlength > $framewidth">
 795        <!-- &#x03bb; -->
 796        <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
 797        <xsl:apply-templates select="m:bvar/m:ci"/>
 798        <xsl:text>:</xsl:text>
 799        <xsl:apply-templates select="m:bvar/m:type">
 800         <xsl:with-param name="current_indent"
 801            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 802        </xsl:apply-templates><br/>
 803        <xsl:call-template name="make_indent">
 804         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 805        </xsl:call-template>
 806        <xsl:text>.</xsl:text>
 807        <xsl:apply-templates select="*[position()=2]">
 808         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 809        </xsl:apply-templates>
 810      </xsl:when>
 811      <xsl:otherwise>
 812       <xsl:apply-templates mode="inline" select="."/>
 813      </xsl:otherwise>
 814      </xsl:choose>
 815 </xsl:template>
 816
 817 <!-- href -->
 818 <xsl:template match="m:ci">
 819  <xsl:choose>
 820   <xsl:when test="boolean(@definitionURL)">
 821    <a>
 822    <xsl:attribute name="href">
 823     <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
 824    </xsl:attribute>
 825    <xsl:apply-templates/>
 826    </a>
 827   </xsl:when>
 828   <xsl:otherwise>
 829    <xsl:value-of select="."/>
 830   </xsl:otherwise>
 831  </xsl:choose>
 832 </xsl:template>
 833
 834 <!-- COUNTING -->
 835
 836 <xsl:template match="m:ci|m:csymbol" mode="charcount">
 837 <xsl:param name="incurrent_length" select="0"/>
 838     <xsl:choose>
 839     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 840      <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>
 841      <xsl:choose>
 842      <xsl:when test="string($siblength) = &quot;&quot;">
 843       <xsl:value-of select="$incurrent_length + string-length()"/>
 844      </xsl:when>
 845      <xsl:otherwise>
 846       <xsl:value-of select="number($siblength)"/>
 847      </xsl:otherwise>
 848      </xsl:choose>
 849     </xsl:when>
 850     <xsl:otherwise>
 851      <xsl:value-of select="$incurrent_length + string-length()"/>
 852     </xsl:otherwise>
 853     </xsl:choose>
 854 </xsl:template>
 855
 856 <xsl:template match="*" mode="charcount">
 857  <xsl:param name="incurrent_length" select="0"/>
 858  <xsl:choose>
 859   <xsl:when test="count(child::*) = 0">
 860    <xsl:value-of select="$incurrent_length"/>
 861   </xsl:when>
 862   <xsl:otherwise>
 863     <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>
 864     <xsl:choose>
 865      <xsl:when test="$framewidth >= number($childlength)">
 866       <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>
 867       <xsl:choose>
 868        <xsl:when test="string($siblength) = &quot;&quot;">
 869         <xsl:value-of select="number($childlength)"/>
 870        </xsl:when>
 871        <xsl:otherwise>
 872         <xsl:value-of select="number($siblength)"/>
 873        </xsl:otherwise>
 874       </xsl:choose>
 875      </xsl:when>
 876      <xsl:otherwise>
 877       <xsl:value-of select="number($childlength)"/>
 878      </xsl:otherwise>
 879     </xsl:choose>
 880   </xsl:otherwise>
 881  </xsl:choose>
 882 </xsl:template>
 883
 884
 885 <!--***********************************************************************-->
 886 <!-- OBJECTS                                                               -->
 887 <!--***********************************************************************-->
 888
 889 <!-- DEFINITION -->
 890
 891 <xsl:template match="Definition">
 892 <xsl:param name="current_indent" select="0"/>
 893 <p>
 894 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 895 TYPE =<br/>
 896       <xsl:call-template name="make_indent">
 897        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 898       </xsl:call-template>
 899        <xsl:apply-templates select="type/*[1]">
 900         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 901        </xsl:apply-templates><br/>
 902 BODY =<br/>
 903       <xsl:call-template name="make_indent">
 904        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 905       </xsl:call-template>
 906        <xsl:apply-templates select="body/*[1]">
 907         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 908        </xsl:apply-templates>
 909 </p>
 910 </xsl:template>
 911
 912 <!-- AXIOM -->
 913
 914 <xsl:template match="Axiom">
 915 <xsl:param name="current_indent" select="0"/>
 916 <p>
 917 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 918 TYPE =<br/>
 919       <xsl:call-template name="make_indent">
 920        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 921       </xsl:call-template>
 922 <xsl:apply-templates select="type/*[1]">
 923           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 924        </xsl:apply-templates>
 925 </p>
 926 </xsl:template>
 927
 928 <!-- UNFINISHED PROOF -->
 929
 930 <xsl:template match="CurrentProof">
 931 <xsl:param name="current_indent" select="0"/>
 932 <p>
 933 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 934 THESIS:  <xsl:apply-templates select="type/*[1]">
 935           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 936          </xsl:apply-templates><br/>
 937 CONJECTURES:
 938       <xsl:for-each select="Conjecture">
 939       <br/>
 940       <xsl:call-template name="make_indent">
 941        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 942       </xsl:call-template>
 943       <xsl:value-of select="./@no"/> :
 944       <xsl:apply-templates select="./*[1]">
 945        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
 946       </xsl:apply-templates>
 947       </xsl:for-each>
 948       <br/>
 949 PROOF:
 950       <xsl:apply-templates select="body/*[1]">
 951         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 952       </xsl:apply-templates>
 953 </p>
 954 </xsl:template>
 955
 956 <!-- MUTUAL INDUCTIVE DEFINITION -->
 957
 958 <xsl:template match="InductiveDefinition">
 959 <xsl:param name="current_indent" select="0"/>
 960 <p>
 961      <xsl:for-each select="InductiveType">
 962          <xsl:choose>
 963          <xsl:when test="position() = 1">
 964           <xsl:choose>
 965           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 966           INDUCTIVE DEFINITION
 967           </xsl:when>
 968           <xsl:otherwise>
 969           COINDUCTIVE DEFINITION
 970           </xsl:otherwise>
 971           </xsl:choose>
 972          </xsl:when>
 973          <xsl:otherwise>
 974           AND
 975          </xsl:otherwise>
 976          </xsl:choose>
 977          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
 978          [
 979           <xsl:if test="string(../Param) != &quot;&quot;">
 980            <xsl:for-each select="../Param">
 981             <xsl:value-of select="./@name"/>
 982             :
 983             <xsl:apply-templates select="*"/>
 984            </xsl:for-each>
 985           </xsl:if>
 986          ] <br/>
 987          OF ARITY
 988          <xsl:apply-templates select="./arity/*[1]">
 989           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 990          </xsl:apply-templates> <br/>
 991          BUILT FROM:
 992       <xsl:for-each select="./Constructor">
 993       <br/>
 994       <xsl:call-template name="make_indent">
 995        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 996       </xsl:call-template>
 997          <xsl:choose>
 998          <xsl:when test="position() = 1">
 999          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1000          </xsl:when>
1001          <xsl:otherwise>
1002          <xsl:text>| </xsl:text>
1003          </xsl:otherwise>
1004          </xsl:choose>
1005          <xsl:value-of select="./@name"/>
1006          <xsl:text>: </xsl:text>
1007          <xsl:apply-templates select="./*[1]">
1008           <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
1009          </xsl:apply-templates>
1010       </xsl:for-each>
1011      </xsl:for-each>
1012 </p>
1013 </xsl:template>
1014
1015 <!-- VARIABLE -->
1016
1017 <xsl:template match="Variable">
1018 <xsl:param name="current_indent" select="0"/>
1019 <p>
1020 VARIABLE <xsl:value-of select="@name"/><br/>
1021 TYPE = <xsl:apply-templates select="type/*[1]">
1022           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1023        </xsl:apply-templates>
1024 </p>
1025 </xsl:template>
1026
1027 <!--***********************************************************************-->
1028 <!-- SECTIONS                                                              -->
1029 <!--***********************************************************************-->
1030
1031 <!-- SECTION -->
1032
1033 <xsl:template match="SECTION">
1034 <xsl:param name="current_indent" select="0"/>
1035  <h1>BEGIN OF SECTION</h1>
1036   <xsl:apply-templates/>
1037  <h1>END OF SECTION</h1>
1038 </xsl:template>
1039
1040 </xsl:stylesheet>