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