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