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