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