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