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, Guidi               -->
  33 <!--***********************************************************************-->
  34
  35 <xsl:param name="CICURI" select="''"/>
  36 <xsl:param name="type" select="'standalone'"/>
  37
  38 <xsl:include href="html_init.xsl"/>
  39 <xsl:include href="html_set.xsl"/>
  40 <xsl:include href="html_reals.xsl"/>
  41
  42 <xsl:variable name="showcast" select="0"/>
  43
  44 <!--***********************************************************************-->
  45 <!-- HTML Head and Body                                                    -->
  46 <!--***********************************************************************-->
  47
  48 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
  49
  50 <!-- document needs method="xml" and searches locally for the dtd if        -->
  51 <!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
  52 <!-- For having output html must be media-type="html" and for having the    -->
  53 <!-- correct <br /> you must specify at least the remote dtd by means of    -->
  54 <!-- doctype-public                                                         -->
  55 <xsl:output
  56         method="xml"
  57         encoding="iso-8859-1"
  58         media-type="text/html"
  59         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  60
  61 <xsl:variable name="framewidth" select="45"/>
  62
  63 <xsl:template match="/">
  64  <xsl:param name="current_indent" select="0"/>
  65  <xsl:choose>
  66   <xsl:when test="$type = 'standalone'">
  67    <html>
  68       <head>
  69          <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
  70          <style> A { text-decoration: none } </style>
  71       </head>
  72       <body bgcolor="white">
  73          <xsl:apply-templates>
  74             <xsl:with-param name="current_indent" select="0"/>
  75          </xsl:apply-templates>
  76       </body>
  77    </html>
  78   </xsl:when>
  79   <xsl:otherwise>
  80    <to_be_embedded>
  81     <xsl:apply-templates>
  82      <xsl:with-param name="current_indent" select="0"/>
  83     </xsl:apply-templates>
  84    </to_be_embedded>
  85   </xsl:otherwise>
  86  </xsl:choose>
  87 </xsl:template>
  88
  89 <!--***********************************************************************-->
  90 <!-- Indentation                                                           -->
  91 <!--***********************************************************************-->
  92
  93 <xsl:template name="make_indent">
  94  <xsl:param name="current_indent" select="0"/>
  95   <xsl:if test="$current_indent > 0">
  96    <xsl:text>&#x00a0;</xsl:text>
  97    <xsl:call-template name="make_indent">
  98     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
  99    </xsl:call-template>
 100   </xsl:if>
 101 </xsl:template>
 102
 103 <!-- Syntactic Sugar -->
 104 <xsl:template match="m:type">
 105 <xsl:param name="current_indent" select="0"/>
 106 <xsl:apply-templates>
 107  <xsl:with-param name="current_indent"
 108            select="$current_indent"/>
 109 </xsl:apply-templates>
 110 </xsl:template>
 111
 112 <xsl:template match="m:condition">
 113 <xsl:param name="current_indent" select="0"/>
 114 <xsl:apply-templates>
 115  <xsl:with-param name="current_indent"
 116            select="$current_indent"/>
 117 </xsl:apply-templates>
 118 </xsl:template>
 119
 120 <xsl:template match="m:math">
 121 <xsl:param name="current_indent" select="0"/>
 122 <xsl:apply-templates>
 123  <xsl:with-param name="current_indent"
 124            select="$current_indent"/>
 125 </xsl:apply-templates>
 126 </xsl:template>
 127
 128 <!--*********************************************************************-->
 129 <!--                         INLINE MODE                                 -->
 130 <!--*********************************************************************-->
 131
 132 <!-- href -->
 133 <xsl:template mode="inline" match="m:ci">
 134  <xsl:choose>
 135   <xsl:when test="boolean(@definitionURL)">
 136    <a href="{@definitionURL}">
 137    <xsl:apply-templates/>
 138    </a>
 139   </xsl:when>
 140   <xsl:otherwise>
 141    <xsl:value-of select="."/>
 142   </xsl:otherwise>
 143  </xsl:choose>
 144 </xsl:template>
 145
 146 <!-- CSYMBOL -->
 147
 148 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 149    <xsl:variable name="name">
 150     <xsl:value-of select="m:csymbol"/>
 151    </xsl:variable>
 152    <xsl:choose>
 153     <!-- FORALL -->
 154     <xsl:when test="$name='forall'">
 155      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 156      <xsl:apply-templates select="m:bvar/m:ci"/>
 157      <xsl:text>:</xsl:text>
 158      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 159      <xsl:text>.</xsl:text>
 160      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 161     </xsl:when>
 162     <xsl:when test="$name='prod'">
 163      <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 164      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 165      <xsl:text>:</xsl:text>
 166      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 167      <xsl:text>.</xsl:text>
 168      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 169     </xsl:when>
 170     <!-- ARROW -->
 171     <xsl:when test="$name='arrow'">
 172      <xsl:text>(</xsl:text>
 173      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 174      <FONT color="blue" SIZE="+0" FACE="symbol">
 175       <xsl:text>&#x00ae;</xsl:text>
 176      </FONT>
 177      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 178      <xsl:text>)</xsl:text>
 179     </xsl:when>
 180     <!-- APP -->
 181     <xsl:when test="$name='app'">
 182      <xsl:text>(</xsl:text>
 183      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 184      <xsl:for-each select="*[position()>2]">
 185       <xsl:text>&#x00A0;</xsl:text>
 186       <xsl:apply-templates mode="inline" select="."/>
 187      </xsl:for-each>
 188      <xsl:text>)</xsl:text>
 189     </xsl:when>
 190     <!-- CAST -->
 191     <xsl:when test="$name='cast'">
 192      <xsl:text>(</xsl:text>
 193      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 194      <xsl:text>:></xsl:text>
 195      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 196      <xsl:text>)</xsl:text>
 197     </xsl:when>
 198     <xsl:when test="$name='Prop'">
 199      <FONT color="violet">Prop</FONT>
 200     </xsl:when>
 201     <xsl:when test="$name='Set'">
 202      <FONT color="violet">Set</FONT>
 203     </xsl:when>
 204     <xsl:when test="$name='Type'">
 205      <FONT color="violet">Type</FONT>
 206     </xsl:when>
 207     <!-- MUTCASE -->
 208     <xsl:when test="$name='mutcase'">
 209      <xsl:text>&lt;</xsl:text>
 210      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 211      <xsl:text>&gt; </xsl:text>
 212      <FONT color="red">CASE </FONT>
 213      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 214      <FONT color="red"> OF </FONT>
 215      <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 216       <xsl:choose>
 217        <xsl:when test="not(position() = 1)">
 218         <xsl:text> | </xsl:text>
 219        </xsl:when>
 220       </xsl:choose>
 221       <xsl:apply-templates mode="inline" select="."/>
 222       <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
 223       <xsl:apply-templates mode="inline"
 224            select="following-sibling::*[position()= 1]"/>
 225      </xsl:for-each>
 226     </xsl:when>
 227     <!-- FIX -->
 228     <xsl:when test="$name='fix'">
 229      <FONT color="red">FIX</FONT>
 230      <xsl:value-of select="m:ci"/>
 231      <xsl:text>{</xsl:text>
 232      <xsl:for-each select="m:bvar">
 233       <xsl:value-of select="m:ci"/>
 234       <xsl:text>:</xsl:text>
 235       <xsl:apply-templates mode="inline" select="m:type"/>
 236       <xsl:text>:=</xsl:text>
 237       <xsl:apply-templates mode="inline"
 238              select="following-sibling::*[position() = 1]"/>
 239       <xsl:choose>
 240        <xsl:when test="position()=last()">
 241         <xsl:text>}</xsl:text>
 242        </xsl:when>
 243        <xsl:otherwise>
 244         <xsl:text>;</xsl:text>
 245        </xsl:otherwise>
 246       </xsl:choose>
 247      </xsl:for-each>
 248     </xsl:when>
 249     <!-- COFIX -->
 250     <xsl:when test="$name='cofix'">
 251      <xsl:text>COFIX</xsl:text>
 252      <xsl:value-of select="m:ci"/>
 253      <xsl:text>{</xsl:text>
 254      <xsl:for-each select="m:bvar">
 255       <xsl:value-of select="m:ci"/>
 256       <xsl:text>:</xsl:text>
 257       <xsl:apply-templates mode="inline" select="m:type"/>
 258       <xsl:text>:=</xsl:text>
 259       <xsl:apply-templates mode="inline"
 260           select="following-sibling::*[position() = 1]"/>
 261       <xsl:choose>
 262        <xsl:when test="position()=last()">
 263         <xsl:text>}</xsl:text>
 264        </xsl:when>
 265        <xsl:otherwise>
 266         <xsl:text>;</xsl:text>
 267        </xsl:otherwise>
 268       </xsl:choose>
 269      </xsl:for-each>
 270     </xsl:when>
 271     <!-- proof -->
 272     <xsl:when test="$name='proof'">
 273        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 274        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 275        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 276     </xsl:when>
 277     <!-- false_ind -->
 278     <xsl:when test="$name='false_ind'">
 279     <xsl:apply-templates mode="inline" select="*[3]"/>
 280     <FONT color="red">Contradiction.</FONT>
 281     </xsl:when>
 282     <!-- and_ind -->
 283     <xsl:when test="$name='and_ind'">
 284      <FONT color="red">From&#x00a0;</FONT>
 285      <xsl:apply-templates select="*[2]"/>
 286      <FONT color="red">&#x00a0;we get</FONT>
 287      (
 288      <xsl:apply-templates select="*[3]"/>
 289      )&#x00a0;
 290      <xsl:apply-templates mode="inline" select="*[4]"/>
 291      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 292      (
 293      <xsl:apply-templates select="*[5]"/>
 294      )&#x00a0;
 295      <xsl:apply-templates mode="inline" select="*[6]"/>
 296      ;
 297      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 298      <xsl:apply-templates mode="inline" select="*[7]"/>
 299     </xsl:when>
 300
 301       <!-- INTERP -->
 302       <xsl:when test="$name='interp'">
 303          <font color="green">[</font>
 304             <xsl:apply-templates select="*[2]"/>
 305          <font color="green">]</font>
 306       </xsl:when>
 307
 308    </xsl:choose>
 309 </xsl:template>
 310
 311 <xsl:template mode="inline" match="m:lambda">
 312       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
 313       <xsl:apply-templates select="m:bvar/m:ci"/>
 314       <xsl:text>:</xsl:text>
 315       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 316       <xsl:text>.</xsl:text>
 317       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 318 </xsl:template>
 319
 320 <!--*********************************************************************-->
 321 <!--                       COUNTING MODE                                 -->
 322 <!--*********************************************************************-->
 323
 324 <xsl:template match="m:apply[m:csymbol]">
 325   <xsl:param name="current_indent" select="0"/>
 326   <xsl:param name="width" select="$framewidth"/>
 327   <xsl:variable name="name">
 328    <xsl:value-of select="m:csymbol"/>
 329   </xsl:variable>
 330   <xsl:variable name="charlength">
 331    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 332   </xsl:variable>
 333      <!-- <xsl:value-of select="$current_indent"/> -->
 334      <!-- <xsl:value-of select="$charlength"/> -->
 335      <xsl:choose>
 336      <!-- FORALL -->
 337       <xsl:when test="$name='forall'">
 338        <xsl:choose>
 339        <xsl:when test="$charlength > $framewidth">
 340          <!-- &#x03a0; -->
 341          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
 342          <xsl:apply-templates select="m:bvar/m:ci"/>
 343          <xsl:text>:</xsl:text>
 344          <xsl:apply-templates select="m:bvar/m:type">
 345           <xsl:with-param name="current_indent"
 346            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 347          </xsl:apply-templates>
 348          <br/>
 349          <xsl:call-template name="make_indent">
 350           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 351          </xsl:call-template>
 352          <xsl:text>.</xsl:text>
 353          <xsl:apply-templates select="*[position()=3]">
 354           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 355          </xsl:apply-templates>
 356        </xsl:when>
 357        <xsl:otherwise>
 358         <xsl:apply-templates mode="inline" select="."/>
 359        </xsl:otherwise>
 360        </xsl:choose>
 361       </xsl:when>
 362       <!-- PROD -->
 363       <xsl:when test="$name='prod'">
 364        <xsl:choose>
 365        <xsl:when test="$charlength > $framewidth">
 366          <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
 367          <xsl:apply-templates select="m:bvar/m:ci"/>
 368          <xsl:text>:</xsl:text>
 369          <xsl:apply-templates select="m:bvar/m:type">
 370           <xsl:with-param name="current_indent"
 371            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 372          </xsl:apply-templates><br/>
 373          <xsl:call-template name="make_indent">
 374           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 375          </xsl:call-template>
 376          <xsl:text>.</xsl:text>
 377          <xsl:apply-templates select="*[position()=3]">
 378           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 379          </xsl:apply-templates>
 380        </xsl:when>
 381        <xsl:otherwise>
 382         <xsl:apply-templates mode="inline" select="."/>
 383        </xsl:otherwise>
 384        </xsl:choose>
 385       </xsl:when>
 386       <!-- ARROW -->
 387       <xsl:when test="$name='arrow'">
 388        <xsl:choose>
 389        <xsl:when test="$charlength > $framewidth">
 390        <xsl:text>(</xsl:text>
 391        <xsl:apply-templates select="*[position()=2]">
 392         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 393        </xsl:apply-templates>
 394        <br/>
 395        <xsl:call-template name="make_indent">
 396         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 397        </xsl:call-template>
 398        <!-- -> -->
 399        <FONT color="blue" SIZE="+0" FACE="symbol">
 400         <xsl:text>&#x00ae;</xsl:text>
 401        </FONT>
 402        <xsl:apply-templates select="*[position()=3]">
 403         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 404        </xsl:apply-templates>
 405        <xsl:text>)</xsl:text>
 406        </xsl:when>
 407        <xsl:otherwise>
 408         <xsl:apply-templates mode="inline" select="."/>
 409        </xsl:otherwise>
 410        </xsl:choose>
 411       </xsl:when>
 412       <!-- APP -->
 413       <xsl:when test="$name='app'">
 414        <xsl:choose>
 415        <xsl:when test="$charlength  > $framewidth">
 416         <xsl:text>(</xsl:text>
 417         <xsl:apply-templates select="*[position()=2]">
 418          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 419         </xsl:apply-templates>
 420          <xsl:for-each select="*[position()>2]">
 421           <br/>
 422            <xsl:call-template name="make_indent">
 423             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 424            </xsl:call-template>
 425             <xsl:apply-templates select=".">
 426              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 427             </xsl:apply-templates>
 428          </xsl:for-each>
 429          <xsl:text>)</xsl:text>
 430        </xsl:when>
 431        <xsl:otherwise>
 432         <xsl:apply-templates mode="inline" select="."/>
 433        </xsl:otherwise>
 434        </xsl:choose>
 435       </xsl:when>
 436       <xsl:when test="$name='cast'">
 437        <xsl:choose>
 438         <xsl:when test="$showcast = 1">
 439          <xsl:choose>
 440           <xsl:when test="$charlength > $framewidth">
 441            <xsl:text>(</xsl:text>
 442            <xsl:apply-templates select="*[position()=2]">
 443             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 444            </xsl:apply-templates><br/>
 445            <xsl:call-template name="make_indent">
 446             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 447            <xsl:text>:></xsl:text>
 448            <xsl:apply-templates select="*[position()=3]">
 449             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 450            </xsl:apply-templates>
 451            <xsl:text>)</xsl:text>
 452           </xsl:when>
 453           <xsl:otherwise>
 454            <xsl:apply-templates mode="inline" select="."/>
 455           </xsl:otherwise>
 456          </xsl:choose>
 457         </xsl:when>
 458         <xsl:otherwise>
 459          <xsl:apply-templates select="*[position()=2]">
 460           <xsl:with-param name="current_indent" select="$current_indent"/>
 461          </xsl:apply-templates>
 462         </xsl:otherwise>
 463        </xsl:choose>
 464       </xsl:when>
 465       <xsl:when test="$name='Prop'">
 466        <xsl:text>Prop</xsl:text>
 467       </xsl:when>
 468       <xsl:when test="$name='Set'">
 469        <xsl:text>Set</xsl:text>
 470       </xsl:when>
 471       <xsl:when test="$name='Type'">
 472        <xsl:text>Type</xsl:text>
 473       </xsl:when>
 474       <xsl:when test="$name='mutcase'">
 475        <xsl:choose>
 476        <xsl:when test="$charlength > $framewidth">
 477          <xsl:text>&lt;</xsl:text>
 478          <xsl:apply-templates select="*[position()=2]">
 479           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 480          </xsl:apply-templates>
 481          <xsl:text>&gt; </xsl:text>
 482          <br/>
 483          <xsl:call-template name="make_indent">
 484           <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
 485          <xsl:text>CASE </xsl:text>
 486          <xsl:apply-templates select="*[position()=3]">
 487           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 488          </xsl:apply-templates>
 489          <xsl:text> OF </xsl:text>
 490          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 491          <br/>
 492          <xsl:call-template name="make_indent">
 493           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 494          </xsl:call-template>
 495             <xsl:choose>
 496             <xsl:when test="position() = 1">
 497              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 498             </xsl:when>
 499             <xsl:otherwise>
 500              <xsl:text>| </xsl:text>
 501             </xsl:otherwise>
 502             </xsl:choose>
 503             <xsl:apply-templates select="."/>
 504             <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
 505             <xsl:variable name="body_size">
 506              <xsl:apply-templates
 507               select="following-sibling::*[1]/*[1]" mode="charcount"/>
 508             </xsl:variable>
 509             <xsl:choose>
 510              <xsl:when test="$body_size > $framewidth">
 511               <br/>
 512               <xsl:call-template name="make_indent">
 513                <xsl:with-param name="current_indent"
 514                     select="$current_indent + 8"/>
 515               </xsl:call-template>
 516               <xsl:apply-templates
 517                    select="following-sibling::*[position()= 1]">
 518               <xsl:with-param name="current_indent"
 519                    select="$current_indent + 8"/>
 520              </xsl:apply-templates>
 521             </xsl:when>
 522             <xsl:otherwise>
 523              <xsl:apply-templates select="following-sibling::*[position()= 1]"
 524                    mode="inline" />
 525             </xsl:otherwise>
 526            </xsl:choose>
 527          </xsl:for-each>
 528        </xsl:when>
 529        <xsl:otherwise>
 530         <xsl:apply-templates mode="inline" select="."/>
 531        </xsl:otherwise>
 532        </xsl:choose>
 533       </xsl:when>
 534       <!-- FIX -->
 535       <xsl:when test="$name='fix'">
 536        <xsl:choose>
 537        <xsl:when test="$charlength  > $framewidth">
 538             <xsl:text>FIX</xsl:text>
 539             <xsl:value-of select="m:ci"/>
 540             <xsl:text>{</xsl:text>
 541             <xsl:for-each select="m:bvar">
 542               <br/>
 543               <xsl:call-template name="make_indent">
 544                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 545               </xsl:call-template>
 546               <xsl:value-of select="m:ci"/>
 547               <xsl:text>:</xsl:text>
 548               <xsl:apply-templates select="m:type">
 549                <xsl:with-param name="current_indent"
 550                     select="$current_indent + 5 + string-length(m:ci)"/>
 551                </xsl:apply-templates>
 552               <br/>
 553               <xsl:call-template name="make_indent">
 554                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 555               </xsl:call-template>
 556               <xsl:text>:=</xsl:text>
 557               <xsl:apply-templates select="following-sibling::*[position() = 1]">
 558                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 559               </xsl:apply-templates>
 560             </xsl:for-each>
 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:when>
 567        <xsl:otherwise>
 568         <xsl:apply-templates mode="inline" select="."/>
 569        </xsl:otherwise>
 570        </xsl:choose>
 571       </xsl:when>
 572       <!-- COFIX -->
 573       <xsl:when test="$name='cofix'">
 574        <xsl:choose>
 575        <xsl:when test="($charlength + 10) > $framewidth">
 576             <xsl:text>COFIX</xsl:text>
 577             <xsl:value-of select="m:ci"/>
 578             <xsl:text>{</xsl:text>
 579             <br/>
 580             <xsl:call-template name="make_indent">
 581              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 582             </xsl:call-template>
 583             <xsl:for-each select="m:bvar">
 584                 <xsl:value-of select="m:ci"/>
 585                 <xsl:text>:</xsl:text>
 586                 <xsl:apply-templates select="m:type">
 587                  <xsl:with-param name="current_indent"
 588                     select="$current_indent + 5 + string-length(m:ci)"/>
 589                 </xsl:apply-templates>
 590                 <br/>
 591                 <xsl:call-template name="make_indent">
 592                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 593                 </xsl:call-template>
 594                 <xsl:text>:=</xsl:text>
 595                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 596                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 597                 </xsl:apply-templates>
 598
 599             </xsl:for-each>
 600             <br/>
 601               <xsl:call-template name="make_indent">
 602                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 603               </xsl:call-template>
 604             <xsl:text>}</xsl:text>
 605        </xsl:when>
 606        <xsl:otherwise>
 607         <xsl:apply-templates mode="inline" select="m:type"/>
 608        </xsl:otherwise>
 609        </xsl:choose>
 610       </xsl:when>
 611       <!-- ***************************************** -->
 612       <!-- *********** PROOF ELEMENTS ************** -->
 613       <!-- ***************************************** -->
 614       <!-- PROOF -->
 615       <xsl:when test="$name='proof'">
 616        <xsl:apply-templates select="*[position()=2]">
 617         <xsl:with-param name="current_indent" select="$current_indent"/>
 618        </xsl:apply-templates>
 619        <br/>
 620        <!-- <xsl:element name="br"/> -->
 621        <xsl:call-template name="make_indent">
 622         <xsl:with-param name="current_indent" select="$current_indent"/>
 623        </xsl:call-template>
 624        <FONT color="red">we proved&#x00a0;</FONT>
 625        <xsl:apply-templates select="*[position()=3]">
 626         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 627        </xsl:apply-templates>
 628       </xsl:when>
 629       <!-- letin1 -->
 630       <xsl:when test="$name='letin1'">
 631        <xsl:apply-templates select="*[position()=2]">
 632         <xsl:with-param name="current_indent" select="$current_indent"/>
 633        </xsl:apply-templates>
 634        <br/>
 635        <xsl:call-template name="make_indent">
 636         <xsl:with-param name="current_indent" select="$current_indent"/>
 637        </xsl:call-template>
 638        <xsl:apply-templates select="*[position()=3]">
 639         <xsl:with-param name="current_indent" select="$current_indent"/>
 640        </xsl:apply-templates>
 641       </xsl:when>
 642       <!-- letin -->
 643       <xsl:when test="$name='letin'">
 644        <xsl:for-each select="*[position()>1 and last()>position()]">
 645         <xsl:apply-templates select=".">
 646          <xsl:with-param name="current_indent" select="$current_indent"/>
 647         </xsl:apply-templates>
 648         <br/>
 649         <xsl:call-template name="make_indent">
 650          <xsl:with-param name="current_indent" select="$current_indent"/>
 651         </xsl:call-template>
 652        </xsl:for-each>
 653        <xsl:apply-templates select="*[position()=last()]">
 654         <xsl:with-param name="current_indent" select="$current_indent"/>
 655        </xsl:apply-templates>
 656       </xsl:when>
 657       <!-- Let -->
 658       <xsl:when test="$name='let'">
 659        (
 660        <xsl:apply-templates select="m:ci"/>
 661        )
 662        <xsl:apply-templates select="*[3]">
 663         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 664        </xsl:apply-templates>
 665       </xsl:when>
 666       <!-- rw_step -->
 667       <xsl:when test="$name='rw_step'">
 668        <xsl:choose>
 669         <xsl:when test="name(*[2])='m:apply'">
 670          <xsl:apply-templates select="*[2]">
 671           <xsl:with-param name="current_indent" select="$current_indent"/>
 672          </xsl:apply-templates>
 673         </xsl:when>
 674         <xsl:otherwise>
 675          <FONT color="red">Consider&#x00a0;</FONT>
 676          <xsl:apply-templates select="*[2]"/>
 677         </xsl:otherwise>
 678        </xsl:choose>
 679        <xsl:variable name="charlength_first">
 680         <xsl:apply-templates select="*[3]/*[1]" mode="charcount"/>
 681        </xsl:variable>
 682        <xsl:variable name="charlength_second">
 683         <xsl:apply-templates select="*[4]/*[1]" mode="charcount"/>
 684        </xsl:variable>
 685        <xsl:variable name="charlength_side_proof">
 686         <xsl:apply-templates select="*[5]/*[1]" mode="charcount"/>
 687        </xsl:variable>
 688        <xsl:variable name="split1"
 689           select="$charlength_first + $charlength_second > $framewidth"/>
 690        <xsl:variable name="split2"
 691           select="$charlength_second + $charlength_side_proof > $framewidth"/>
 692      <!-- <xsl:value-of select="$current_indent"/> -->
 693      <!-- <xsl:value-of select="$charlength"/> -->
 694        <br/>
 695        <xsl:call-template name="make_indent">
 696         <xsl:with-param name="current_indent" select="$current_indent"/>
 697        </xsl:call-template>
 698        <FONT color="red">Rewrite&#x00a0;</FONT>
 699        <xsl:apply-templates mode="inline" select="*[3]"/>
 700        <xsl:text>&#x00a0;</xsl:text>
 701        <xsl:if test="$split1">
 702        <br/>
 703        <xsl:call-template name="make_indent">
 704         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 705        </xsl:call-template>
 706        </xsl:if>
 707        <FONT color="red">with&#x00a0;</FONT>
 708        <xsl:apply-templates mode="inline" select="*[4]"/>
 709        <xsl:text>&#x00a0;</xsl:text>
 710        <xsl:if test="$split2">
 711        <br/>
 712        <xsl:call-template name="make_indent">
 713         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 714        </xsl:call-template>
 715        </xsl:if>
 716        <FONT color="red">by&#x00a0;</FONT>
 717        <xsl:apply-templates select="*[5]">
 718         <xsl:with-param name="current_indent" select="$current_indent+7"/>
 719        </xsl:apply-templates>
 720       </xsl:when>
 721       <!-- rewrite and apply -->
 722       <xsl:when test="$name='rewrite_and_apply'">
 723        <xsl:apply-templates select="*[2]">
 724         <xsl:with-param name="current_indent" select="$current_indent"/>
 725        </xsl:apply-templates>
 726        <br/>
 727        <xsl:call-template name="make_indent">
 728         <xsl:with-param name="current_indent" select="$current_indent"/>
 729        </xsl:call-template>
 730        <FONT color="red">Then apply it to&#x00a0;</FONT>
 731        <xsl:apply-templates select="*[position()>2]"/>
 732       </xsl:when>
 733       <!-- by_induction -->
 734       <xsl:when test="$name='by_induction'">
 735        <FONT color="red">We prove&#x00a0;</FONT>
 736        <xsl:apply-templates select="../*[3]">
 737         <xsl:with-param name="current_indent" select="$current_indent+18"/>
 738        </xsl:apply-templates>
 739        <br/>
 740        <xsl:call-template name="make_indent">
 741         <xsl:with-param name="current_indent" select="$current_indent"/>
 742        </xsl:call-template>
 743        <FONT color="red">by induction on&#x00a0;</FONT>
 744        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
 745         <xsl:with-param name="current_indent" select="$current_indent+30"/>
 746        </xsl:apply-templates>
 747        <!--
 748        <br/>
 749        <xsl:call-template name="make_indent">
 750         <xsl:with-param name="current_indent" select="$current_indent"/>
 751        </xsl:call-template>
 752        <xsl:text>The induction property is</xsl:text>
 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="*[3]">
 758         <xsl:with-param name="current_indent" select="$current_indent"/>
 759        </xsl:apply-templates>
 760        -->
 761        <xsl:apply-templates
 762             select="*[position()>3 and not(position()=last())]">
 763         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 764        </xsl:apply-templates>
 765        <!-- <br/>
 766        <xsl:call-template name="make_indent">
 767         <xsl:with-param name="current_indent" select="$current_indent"/>
 768        </xsl:call-template>
 769        <xsl:text>End induction</xsl:text> -->
 770       </xsl:when>
 771       <!-- inductive_case -->
 772       <xsl:when test="$name='inductive_case'">
 773        <br/>
 774        <xsl:call-template name="make_indent">
 775         <xsl:with-param name="current_indent" select="$current_indent"/>
 776        </xsl:call-template>
 777        <FONT color="red">Case&#x00a0;</FONT>
 778        <xsl:apply-templates select="*[2]">
 779         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 780        </xsl:apply-templates>
 781        <xsl:if test="*[3]/*[position()>1]">
 782         <br/>
 783         <xsl:call-template name="make_indent">
 784          <xsl:with-param name="current_indent" select="$current_indent+4"/>
 785         </xsl:call-template>
 786         <FONT color="red">By induction hypothesis, we have:</FONT>
 787         <xsl:for-each select="*[3]/*[position()>1]">
 788          <br/>
 789          <xsl:call-template name="make_indent">
 790           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 791          </xsl:call-template>
 792          <xsl:text>(</xsl:text>
 793          <xsl:apply-templates select="m:ci"/>
 794          <xsl:text>)&#x00a0;</xsl:text>
 795          <xsl:apply-templates select="m:type">
 796           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 797          </xsl:apply-templates>
 798         </xsl:for-each>
 799        </xsl:if>
 800        <br/>
 801         <xsl:call-template name="make_indent">
 802          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 803         </xsl:call-template>
 804        <xsl:apply-templates select="*[4]">
 805         <xsl:with-param name="current_indent" select="$current_indent +4"/>
 806        </xsl:apply-templates>
 807        <!-- <br/>
 808        <xsl:call-template name="make_indent">
 809         <xsl:with-param name="current_indent" select="$current_indent"/>
 810        </xsl:call-template>
 811        <xsl:text>End Case</xsl:text> -->
 812       </xsl:when>
 813       <!-- case_lhs  -->
 814       <xsl:when test="$name='case_lhs'">
 815        <xsl:choose>
 816         <xsl:when test="count(*)=2">
 817          <xsl:apply-templates mode="inline" select="*[2]"/>
 818         </xsl:when>
 819         <xsl:otherwise>
 820          <xsl:text>(</xsl:text>
 821          <xsl:apply-templates mode="inline" select="*[2]"/>
 822          <xsl:for-each select="m:bvar">
 823           <xsl:text>&#x00a0;</xsl:text>
 824           <xsl:apply-templates mode="inline" select="*[1]"/>
 825           <xsl:text>:</xsl:text>
 826           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
 827          </xsl:for-each>
 828          <xsl:text>)</xsl:text>
 829         </xsl:otherwise>
 830        </xsl:choose>
 831       </xsl:when>
 832       <!-- nat_ind -->
 833       <xsl:when test="$name='nat_ind_complete'">
 834        <FONT color="red">By induction on&#x00a0;</FONT>
 835        <xsl:apply-templates select="*[2]"/>:
 836        <br/>
 837        <xsl:call-template name="make_indent">
 838         <xsl:with-param name="current_indent" select="$current_indent"/>
 839        </xsl:call-template>
 840        <xsl:text>0&#x00a0;</xsl:text>
 841        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 842        <xsl:apply-templates select="*[3]">
 843         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 844        </xsl:apply-templates>
 845        <br/>
 846        <xsl:call-template name="make_indent">
 847         <xsl:with-param name="current_indent" select="$current_indent"/>
 848        </xsl:call-template>
 849        <xsl:text>S(</xsl:text>
 850        <xsl:apply-templates select="*[4]"/>
 851        <xsl:text>)&#x00a0;</xsl:text>
 852        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 853        <FONT color="red">Assume by induction</FONT>
 854        <br/>
 855        <xsl:call-template name="make_indent">
 856         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 857        </xsl:call-template>
 858        <xsl:text>(</xsl:text>
 859        <xsl:apply-templates select="*[5]"/>
 860        <xsl:text>)</xsl:text>
 861        <xsl:apply-templates select="*[6]">
 862         <xsl:with-param name="current_indent" select="$current_indent + 14"/>
 863        </xsl:apply-templates>
 864        <br/>
 865        <xsl:call-template name="make_indent">
 866         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 867        </xsl:call-template>
 868        <xsl:apply-templates select="*[7]">
 869         <xsl:with-param name="current_indent" select="$current_indent + 10"/>
 870        </xsl:apply-templates>
 871       </xsl:when>
 872       <!-- false_ind -->
 873       <xsl:when test="$name='false_ind'">
 874        <xsl:apply-templates select="*[3]">
 875         <xsl:with-param name="current_indent" select="$current_indent"/>
 876        </xsl:apply-templates>
 877        <br/>
 878        <xsl:call-template name="make_indent">
 879         <xsl:with-param name="current_indent" select="$current_indent"/>
 880        </xsl:call-template>
 881        <FONT color="red">Contradiction.</FONT>
 882       </xsl:when>
 883       <!-- and_ind -->
 884       <xsl:when test="$name='and_ind'">
 885        <xsl:choose>
 886         <xsl:when test="name(*[2])='m:apply'">
 887          <xsl:apply-templates select="*[2]">
 888           <xsl:with-param name="current_indent" select="$current_indent"/>
 889          </xsl:apply-templates>
 890         </xsl:when>
 891         <xsl:otherwise>
 892          <FONT color="red">Consider&#x00a0;</FONT>
 893          <xsl:apply-templates select="*[2]"/>
 894         </xsl:otherwise>
 895        </xsl:choose>
 896        <br/>
 897        <xsl:call-template name="make_indent">
 898         <xsl:with-param name="current_indent" select="$current_indent"/>
 899        </xsl:call-template>
 900        <FONT color="red">In particular, we have</FONT>
 901        <br/>
 902        <xsl:call-template name="make_indent">
 903         <xsl:with-param name="current_indent" select="$current_indent"/>
 904        </xsl:call-template>
 905        (
 906        <xsl:apply-templates select="*[3]"/>
 907        )&#x00a0;
 908        <xsl:apply-templates select="*[4]">
 909         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 910        </xsl:apply-templates>
 911        <br/>
 912        <xsl:call-template name="make_indent">
 913         <xsl:with-param name="current_indent" select="$current_indent"/>
 914        </xsl:call-template>
 915        (
 916        <xsl:apply-templates select="*[5]"/>
 917        )&#x00a0;
 918        <xsl:apply-templates select="*[6]">
 919         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 920        </xsl:apply-templates>
 921        <br/>
 922        <xsl:call-template name="make_indent">
 923         <xsl:with-param name="current_indent" select="$current_indent"/>
 924        </xsl:call-template>
 925        <xsl:apply-templates select="*[7]">
 926         <xsl:with-param name="current_indent" select="$current_indent"/>
 927        </xsl:apply-templates>
 928       </xsl:when>
 929       <!-- full_or_ind -->
 930       <xsl:when test="$name='full_or_ind'">
 931        <xsl:choose>
 932         <xsl:when test="name(*[2])='m:apply'">
 933          <xsl:apply-templates select="*[2]">
 934           <xsl:with-param name="current_indent" select="$current_indent"/>
 935          </xsl:apply-templates>
 936         </xsl:when>
 937         <xsl:otherwise>
 938          <FONT color="red">Consider&#x00a0;</FONT>
 939          <xsl:apply-templates select="*[2]"/>
 940         </xsl:otherwise>
 941        </xsl:choose>
 942        <br/>
 943        <xsl:call-template name="make_indent">
 944         <xsl:with-param name="current_indent" select="$current_indent"/>
 945        </xsl:call-template>
 946        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
 947        <xsl:apply-templates select="*[3]"/>
 948        <br/>
 949        <xsl:call-template name="make_indent">
 950         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 951        </xsl:call-template>
 952        <FONT color="red">Left: suppose&#x00a0;</FONT>
 953        <xsl:text>(</xsl:text>
 954        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
 955        <xsl:text>)&#x00a0;</xsl:text>
 956        <xsl:apply-templates
 957             select="*[4]/m:bvar/m:type/*[1]"/>
 958        <br/>
 959        <xsl:call-template name="make_indent">
 960         <xsl:with-param name="current_indent" select="$current_indent+15"/>
 961        </xsl:call-template>
 962        <xsl:apply-templates
 963             select="*[4]/*[3]">
 964         <xsl:with-param name="current_indent" select="$current_indent+15"/>
 965        </xsl:apply-templates>
 966        <br/>
 967        <xsl:call-template name="make_indent">
 968         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 969        </xsl:call-template>
 970        <FONT color="red">Right: suppose&#x00a0;</FONT>
 971        <xsl:text>(</xsl:text>
 972        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
 973        <xsl:text>)&#x00a0;</xsl:text>
 974        <xsl:apply-templates
 975             select="*[5]/m:bvar/m:type/*[1]"/>
 976        <br/>
 977        <xsl:call-template name="make_indent">
 978         <xsl:with-param name="current_indent" select="$current_indent+16"/>
 979        </xsl:call-template>
 980        <xsl:apply-templates
 981             select="*[5]/*[3]">
 982         <xsl:with-param name="current_indent" select="$current_indent+16"/>
 983        </xsl:apply-templates>
 984       </xsl:when>
 985       <!-- or_ind -->
 986       <xsl:when test="$name='or_ind'">
 987        <xsl:choose>
 988         <xsl:when test="name(*[2])='m:apply'">
 989          <xsl:apply-templates select="*[2]">
 990           <xsl:with-param name="current_indent" select="$current_indent"/>
 991          </xsl:apply-templates>
 992         </xsl:when>
 993         <xsl:otherwise>
 994          <FONT color="red">Consider&#x00a0;</FONT>
 995          <xsl:apply-templates select="*[2]"/>
 996         </xsl:otherwise>
 997        </xsl:choose>
 998        <br/>
 999        <xsl:call-template name="make_indent">
1000         <xsl:with-param name="current_indent" select="$current_indent"/>
1001        </xsl:call-template>
1002        <FONT color="red">We prove&#x00a0;</FONT>
1003        <xsl:apply-templates select="*[3]"/>
1004        <FONT color="red">&#x00a0;by cases:</FONT>
1005        <br/>
1006        <xsl:call-template name="make_indent">
1007         <xsl:with-param name="current_indent" select="$current_indent"/>
1008        </xsl:call-template>
1009        *
1010        <xsl:apply-templates select="*[4]">
1011         <xsl:with-param name="current_indent" select="$current_indent"/>
1012        </xsl:apply-templates>
1013        <br/>
1014        <xsl:call-template name="make_indent">
1015         <xsl:with-param name="current_indent" select="$current_indent"/>
1016        </xsl:call-template>
1017        *
1018        <xsl:apply-templates select="*[5]">
1019         <xsl:with-param name="current_indent" select="$current_indent"/>
1020        </xsl:apply-templates>
1021       </xsl:when>
1022       <!-- Ex_ind -->
1023       <xsl:when test="$name='ex_ind'">
1024        <xsl:choose>
1025         <xsl:when test="name(*[2])='m:apply'">
1026          <xsl:apply-templates select="*[2]">
1027           <xsl:with-param name="current_indent" select="$current_indent"/>
1028          </xsl:apply-templates>
1029         </xsl:when>
1030         <xsl:otherwise>
1031          <FONT color="red">Consider&#x00a0;</FONT>
1032          <xsl:apply-templates select="*[2]">
1033           <xsl:with-param name="current_indent" select="$current_indent"/>
1034          </xsl:apply-templates>
1035         </xsl:otherwise>
1036        </xsl:choose>
1037        <br/>
1038        <xsl:call-template name="make_indent">
1039         <xsl:with-param name="current_indent" select="$current_indent"/>
1040        </xsl:call-template>
1041        <FONT color="red">Let&#x00a0;</FONT>
1042        <xsl:apply-templates mode="inline" select="*[3]"/>
1043        :
1044        <xsl:apply-templates mode="inline" select="*[4]"/>
1045        <FONT color="red">&#x00a0;such that</FONT>
1046        <br/>
1047        <xsl:call-template name="make_indent">
1048         <xsl:with-param name="current_indent" select="$current_indent"/>
1049        </xsl:call-template>
1050        (
1051        <xsl:apply-templates mode="inline" select="*[5]"/>
1052        )
1053        <xsl:apply-templates select="*[6]">
1054         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1055        </xsl:apply-templates>
1056        <br/>
1057        <xsl:call-template name="make_indent">
1058         <xsl:with-param name="current_indent" select="$current_indent"/>
1059        </xsl:call-template>
1060        <xsl:apply-templates select="*[7]">
1061         <xsl:with-param name="current_indent" select="$current_indent"/>
1062        </xsl:apply-templates>
1063       </xsl:when>
1064
1065       <!-- INTERP -->
1066       <xsl:when test="$name='interp'">
1067          <font color="green">[</font>
1068             <xsl:apply-templates select="*[2]"/>
1069          <font color="green">]</font>
1070       </xsl:when>
1071
1072      </xsl:choose>
1073 </xsl:template>
1074
1075 <!-- LAMBDA -->
1076
1077 <xsl:template match="m:lambda">
1078 <xsl:param name="current_indent" select="0"/>
1079     <xsl:variable name="charlength">
1080      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1081      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1082     </xsl:variable>
1083     <!-- <xsl:value-of select="$charlength"/> -->
1084     <!-- <xsl:value-of select="$current_indent"/> -->
1085      <xsl:choose>
1086      <xsl:when test="$charlength > $framewidth">
1087        <!-- &#x03bb; -->
1088        <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
1089        <xsl:apply-templates select="m:bvar/m:ci"/>
1090        <xsl:text>:</xsl:text>
1091        <xsl:apply-templates select="m:bvar/m:type">
1092         <xsl:with-param name="current_indent"
1093            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1094        </xsl:apply-templates><br/>
1095        <xsl:call-template name="make_indent">
1096         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1097        </xsl:call-template>
1098        <xsl:text>.</xsl:text>
1099        <xsl:apply-templates select="*[position()=2]">
1100         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1101        </xsl:apply-templates>
1102      </xsl:when>
1103      <xsl:otherwise>
1104       <xsl:apply-templates mode="inline" select="."/>
1105      </xsl:otherwise>
1106      </xsl:choose>
1107 </xsl:template>
1108
1109 <!-- href -->
1110 <xsl:template match="m:ci">
1111  <xsl:choose>
1112   <xsl:when test="boolean(@definitionURL)">
1113    <a href="{@definitionURL}">
1114    <xsl:apply-templates/>
1115    </a>
1116   </xsl:when>
1117   <xsl:otherwise>
1118    <xsl:value-of select="."/>
1119   </xsl:otherwise>
1120  </xsl:choose>
1121 </xsl:template>
1122
1123 <!-- COUNTING -->
1124
1125 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1126 <xsl:param name="incurrent_length" select="0"/>
1127     <xsl:choose>
1128     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1129      <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>
1130      <xsl:choose>
1131      <xsl:when test="string($siblength) = &quot;&quot;">
1132       <xsl:value-of select="$incurrent_length + string-length()"/>
1133      </xsl:when>
1134      <xsl:otherwise>
1135       <xsl:value-of select="number($siblength)"/>
1136      </xsl:otherwise>
1137      </xsl:choose>
1138     </xsl:when>
1139     <xsl:otherwise>
1140      <xsl:value-of select="$incurrent_length + string-length()"/>
1141     </xsl:otherwise>
1142     </xsl:choose>
1143 </xsl:template>
1144
1145 <xsl:template match="*" mode="charcount">
1146  <xsl:param name="incurrent_length" select="0"/>
1147  <xsl:choose>
1148   <xsl:when test="count(child::*) = 0">
1149    <xsl:value-of select="$incurrent_length"/>
1150   </xsl:when>
1151   <xsl:otherwise>
1152     <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>
1153     <xsl:choose>
1154      <xsl:when test="$framewidth >= number($childlength)">
1155       <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>
1156       <xsl:choose>
1157        <xsl:when test="string($siblength) = &quot;&quot;">
1158         <xsl:value-of select="number($childlength)"/>
1159        </xsl:when>
1160        <xsl:otherwise>
1161         <xsl:value-of select="number($siblength)"/>
1162        </xsl:otherwise>
1163       </xsl:choose>
1164      </xsl:when>
1165      <xsl:otherwise>
1166       <xsl:value-of select="number($childlength)"/>
1167      </xsl:otherwise>
1168     </xsl:choose>
1169   </xsl:otherwise>
1170  </xsl:choose>
1171 </xsl:template>
1172
1173
1174 <!--***********************************************************************-->
1175 <!-- OBJECTS                                                               -->
1176 <!--***********************************************************************-->
1177
1178 <!-- DEFINITION -->
1179
1180 <xsl:template match="Definition">
1181 <xsl:param name="current_indent" select="0"/>
1182 <p>
1183 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1184 TYPE =<br/>
1185       <xsl:call-template name="make_indent">
1186        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1187       </xsl:call-template>
1188        <xsl:apply-templates select="type/*[1]">
1189         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1190        </xsl:apply-templates><br/>
1191 BODY =<br/>
1192       <xsl:call-template name="make_indent">
1193        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1194       </xsl:call-template>
1195        <xsl:apply-templates select="body/*[1]">
1196         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1197        </xsl:apply-templates>
1198 </p>
1199 </xsl:template>
1200
1201 <!-- AXIOM -->
1202
1203 <xsl:template match="Axiom">
1204 <xsl:param name="current_indent" select="0"/>
1205 <p>
1206 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1207 TYPE =<br/>
1208       <xsl:call-template name="make_indent">
1209        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1210       </xsl:call-template>
1211 <xsl:apply-templates select="type/*[1]">
1212           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1213        </xsl:apply-templates>
1214 </p>
1215 </xsl:template>
1216
1217 <!-- UNFINISHED PROOF -->
1218
1219 <xsl:template match="CurrentProof">
1220 <xsl:param name="current_indent" select="0"/>
1221 <p>
1222 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1223 THESIS:  <xsl:apply-templates select="type/*[1]">
1224           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1225          </xsl:apply-templates><br/>
1226 CONJECTURES:
1227       <xsl:for-each select="Conjecture">
1228       <br/>
1229       <xsl:call-template name="make_indent">
1230        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1231       </xsl:call-template>
1232       <xsl:value-of select="./@no"/> :
1233       <xsl:apply-templates select="./*[1]">
1234        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
1235       </xsl:apply-templates>
1236       </xsl:for-each>
1237       <br/>
1238 PROOF:
1239       <xsl:apply-templates select="body/*[1]">
1240         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1241       </xsl:apply-templates>
1242 </p>
1243 </xsl:template>
1244
1245 <!-- MUTUAL INDUCTIVE DEFINITION -->
1246
1247 <xsl:template match="InductiveDefinition">
1248 <xsl:param name="current_indent" select="0"/>
1249 <p>
1250      <xsl:for-each select="InductiveType">
1251          <xsl:choose>
1252          <xsl:when test="position() = 1">
1253           <xsl:choose>
1254           <xsl:when test="string(./@inductive) = &quot;true&quot;">
1255           INDUCTIVE DEFINITION
1256           </xsl:when>
1257           <xsl:otherwise>
1258           COINDUCTIVE DEFINITION
1259           </xsl:otherwise>
1260           </xsl:choose>
1261          </xsl:when>
1262          <xsl:otherwise>
1263           AND
1264          </xsl:otherwise>
1265          </xsl:choose>
1266          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
1267          [
1268           <xsl:if test="string(../Param) != &quot;&quot;">
1269            <xsl:for-each select="../Param">
1270             <xsl:value-of select="./@name"/>
1271             :
1272             <xsl:apply-templates select="*"/>
1273            </xsl:for-each>
1274           </xsl:if>
1275          ] <br/>
1276          OF ARITY
1277          <xsl:apply-templates select="./arity/*[1]">
1278           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1279          </xsl:apply-templates> <br/>
1280          BUILT FROM:
1281       <xsl:for-each select="./Constructor">
1282       <br/>
1283       <xsl:call-template name="make_indent">
1284        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1285       </xsl:call-template>
1286          <xsl:choose>
1287          <xsl:when test="position() = 1">
1288          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1289          </xsl:when>
1290          <xsl:otherwise>
1291          <xsl:text>| </xsl:text>
1292          </xsl:otherwise>
1293          </xsl:choose>
1294          <xsl:value-of select="./@name"/>
1295          <xsl:text>: </xsl:text>
1296          <xsl:apply-templates select="./*[1]">
1297           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1298          </xsl:apply-templates>
1299       </xsl:for-each>
1300      </xsl:for-each>
1301 </p>
1302 </xsl:template>
1303
1304 <!-- VARIABLE -->
1305
1306 <xsl:template match="Variable">
1307 <xsl:param name="current_indent" select="0"/>
1308 <p>
1309 VARIABLE <xsl:value-of select="@name"/><br/>
1310 TYPE = <xsl:apply-templates select="type/*[1]">
1311           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1312        </xsl:apply-templates>
1313 </p>
1314 </xsl:template>
1315
1316 <!--***********************************************************************-->
1317 <!-- SECTIONS                                                              -->
1318 <!--***********************************************************************-->
1319
1320 <!-- SECTION -->
1321
1322 <xsl:template match="SECTION">
1323 <xsl:param name="current_indent" select="0"/>
1324  <h1>BEGIN OF SECTION</h1>
1325   <xsl:apply-templates/>
1326  <h1>END OF SECTION</h1>
1327 </xsl:template>
1328
1329 </xsl:stylesheet>