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