helm/style/content_to_html.xsl

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