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          <xsl:text>CASE </xsl:text>
 471          <xsl:apply-templates select="*[position()=3]">
 472           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 473          </xsl:apply-templates>
 474          <xsl:text> OF </xsl:text>
 475          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 476          <br/>
 477          <xsl:call-template name="make_indent">
 478             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 479          </xsl:call-template>
 480             <xsl:choose>
 481             <xsl:when test="position() = 1">
 482              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 483             </xsl:when>
 484             <xsl:otherwise>
 485              <xsl:text>| </xsl:text>
 486             </xsl:otherwise>
 487             </xsl:choose>
 488             <xsl:apply-templates select="."/>
 489             <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
 490             <xsl:apply-templates select="following-sibling::*[position()= 1]">
 491              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
 492             </xsl:apply-templates>
 493          </xsl:for-each>
 494        </xsl:when>
 495        <xsl:otherwise>
 496         <xsl:apply-templates mode="inline" select="."/>
 497        </xsl:otherwise>
 498        </xsl:choose>
 499       </xsl:when>
 500       <!-- FIX -->
 501       <xsl:when test="$name='fix'">
 502        <xsl:choose>
 503        <xsl:when test="$charlength  > $framewidth">
 504             <xsl:text>FIX</xsl:text>
 505             <xsl:value-of select="m:ci"/>
 506             <xsl:text>{</xsl:text>
 507             <xsl:for-each select="m:bvar">
 508               <br/>
 509               <xsl:call-template name="make_indent">
 510                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 511               </xsl:call-template>
 512               <xsl:value-of select="m:ci"/>
 513               <xsl:text>:</xsl:text>
 514               <xsl:apply-templates select="m:type">
 515                <xsl:with-param name="current_indent"
 516                     select="$current_indent + 5 + string-length(m:ci)"/>
 517                </xsl:apply-templates>
 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:apply-templates select="following-sibling::*[position() = 1]">
 524                <xsl:with-param name="current_indent" select="$current_indent +2"/>
 525               </xsl:apply-templates>
 526             </xsl:for-each>
 527              <br/>
 528               <xsl:call-template name="make_indent">
 529                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 530               </xsl:call-template>
 531            <xsl:text>}</xsl:text>
 532        </xsl:when>
 533        <xsl:otherwise>
 534         <xsl:apply-templates mode="inline" select="."/>
 535        </xsl:otherwise>
 536        </xsl:choose>
 537       </xsl:when>
 538       <!-- COFIX -->
 539       <xsl:when test="$name='cofix'">
 540        <xsl:choose>
 541        <xsl:when test="($charlength + 10) > $framewidth">
 542             <xsl:text>COFIX</xsl:text>
 543             <xsl:value-of select="m:ci"/>
 544             <xsl:text>{</xsl:text>
 545             <br/>
 546             <xsl:call-template name="make_indent">
 547              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 548             </xsl:call-template>
 549             <xsl:for-each select="m:bvar">
 550                 <xsl:value-of select="m:ci"/>
 551                 <xsl:text>:</xsl:text>
 552                 <xsl:apply-templates select="m:type">
 553                  <xsl:with-param name="current_indent"
 554                     select="$current_indent + 5 + string-length(m:ci)"/>
 555                 </xsl:apply-templates>
 556                 <br/>
 557                 <xsl:call-template name="make_indent">
 558                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 559                 </xsl:call-template>
 560                 <xsl:text>:=</xsl:text>
 561                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
 562                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 563                 </xsl:apply-templates>
 564
 565             </xsl:for-each>
 566             <br/>
 567               <xsl:call-template name="make_indent">
 568                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 569               </xsl:call-template>
 570             <xsl:text>}</xsl:text>
 571        </xsl:when>
 572        <xsl:otherwise>
 573         <xsl:apply-templates mode="inline" select="m:type"/>
 574        </xsl:otherwise>
 575        </xsl:choose>
 576       </xsl:when>
 577       <!-- ***************************************** -->
 578       <!-- *********** PROOF ELEMENTS ************** -->
 579       <!-- ***************************************** -->
 580       <!-- PROOF -->
 581       <xsl:when test="$name='proof'">
 582        <xsl:apply-templates select="*[position()=2]">
 583         <xsl:with-param name="current_indent" select="$current_indent"/>
 584        </xsl:apply-templates>
 585        <br/>
 586        <!-- <xsl:element name="br"/> -->
 587        <xsl:call-template name="make_indent">
 588         <xsl:with-param name="current_indent" select="$current_indent"/>
 589        </xsl:call-template>
 590        <FONT color="red">we proved&#x00a0;</FONT>
 591        <xsl:apply-templates select="*[position()=3]">
 592         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 593        </xsl:apply-templates>
 594       </xsl:when>
 595       <!-- letin1 -->
 596       <xsl:when test="$name='letin1'">
 597        <xsl:apply-templates select="*[position()=2]">
 598         <xsl:with-param name="current_indent" select="$current_indent"/>
 599        </xsl:apply-templates>
 600        <br/>
 601        <xsl:call-template name="make_indent">
 602         <xsl:with-param name="current_indent" select="$current_indent"/>
 603        </xsl:call-template>
 604        <xsl:apply-templates select="*[position()=3]">
 605         <xsl:with-param name="current_indent" select="$current_indent"/>
 606        </xsl:apply-templates>
 607       </xsl:when>
 608       <!-- letin -->
 609       <xsl:when test="$name='letin'">
 610        <xsl:for-each select="*[position()>1 and last()>position()]">
 611         <xsl:apply-templates select=".">
 612          <xsl:with-param name="current_indent" select="$current_indent"/>
 613         </xsl:apply-templates>
 614         <br/>
 615         <xsl:call-template name="make_indent">
 616          <xsl:with-param name="current_indent" select="$current_indent"/>
 617         </xsl:call-template>
 618        </xsl:for-each>
 619        <xsl:apply-templates select="*[position()=last()]">
 620         <xsl:with-param name="current_indent" select="$current_indent"/>
 621        </xsl:apply-templates>
 622       </xsl:when>
 623       <!-- Let -->
 624       <xsl:when test="$name='let'">
 625        (
 626        <xsl:apply-templates select="m:ci"/>
 627        )
 628        <xsl:apply-templates select="*[3]">
 629         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 630        </xsl:apply-templates>
 631       </xsl:when>
 632       <!-- rw_step -->
 633       <xsl:when test="$name='rw_step'">
 634        <xsl:choose>
 635         <xsl:when test="name(*[2])='m:apply'">
 636          <xsl:apply-templates select="*[2]">
 637           <xsl:with-param name="current_indent" select="$current_indent"/>
 638          </xsl:apply-templates>
 639         </xsl:when>
 640         <xsl:otherwise>
 641          <FONT color="red">Consider&#x00a0;</FONT>
 642          <xsl:apply-templates select="*[2]"/>
 643         </xsl:otherwise>
 644        </xsl:choose>
 645        <xsl:variable name="charlength_first">
 646         <xsl:apply-templates select="*[3]" mode="charcount"/>
 647        </xsl:variable>
 648        <xsl:variable name="charlength_second">
 649         <xsl:apply-templates select="*[4]" mode="charcount"/>
 650        </xsl:variable>
 651        <xsl:variable name="charlength_side_proof">
 652         <xsl:apply-templates select="*[5]" mode="charcount"/>
 653        </xsl:variable>
 654        <xsl:variable name="split1"
 655           select="$charlength_first + $charlength_second > $framewidth"/>
 656        <xsl:variable name="split2"
 657           select="$charlength_second + $charlength_side_proof > $framewidth"/>
 658      <!-- <xsl:value-of select="$current_indent"/> -->
 659      <!-- <xsl:value-of select="$charlength"/> -->
 660        <br/>
 661        <xsl:call-template name="make_indent">
 662         <xsl:with-param name="current_indent" select="$current_indent"/>
 663        </xsl:call-template>
 664        <FONT color="red">Rewrite&#x00a0;</FONT>
 665        <xsl:apply-templates mode="inline" select="*[3]"/>
 666        <xsl:text>&#x00a0;</xsl:text>
 667        <xsl:if test="$split1">
 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">with&#x00a0;</FONT>
 674        <xsl:apply-templates mode="inline" select="*[4]"/>
 675        <xsl:text>&#x00a0;</xsl:text>
 676        <xsl:if test="$split2">
 677        <br/>
 678        <xsl:call-template name="make_indent">
 679         <xsl:with-param name="current_indent" select="$current_indent"/>
 680        </xsl:call-template>
 681        </xsl:if>
 682        <FONT color="red">by&#x00a0;</FONT>
 683        <xsl:apply-templates select="*[5]">
 684         <xsl:with-param name="current_indent" select="$current_indent+5"/>
 685        </xsl:apply-templates>
 686       </xsl:when>
 687       <!-- rewrite and apply -->
 688       <xsl:when test="$name='rewrite_and_apply'">
 689        <xsl:apply-templates select="*[2]">
 690         <xsl:with-param name="current_indent" select="$current_indent"/>
 691        </xsl:apply-templates>
 692        <br/>
 693        <xsl:call-template name="make_indent">
 694         <xsl:with-param name="current_indent" select="$current_indent"/>
 695        </xsl:call-template>
 696        <FONT color="red">Then apply it to&#x00a0;</FONT>
 697        <xsl:apply-templates select="*[position()>2]"/>
 698       </xsl:when>
 699       <!-- by_induction -->
 700       <xsl:when test="$name='by_induction'">
 701        <FONT color="red">We prove&#x00a0;</FONT>
 702        <xsl:apply-templates select="../*[3]">
 703         <xsl:with-param name="current_indent" select="$current_indent+18"/>
 704        </xsl:apply-templates>
 705        <br/>
 706        <xsl:call-template name="make_indent">
 707         <xsl:with-param name="current_indent" select="$current_indent"/>
 708        </xsl:call-template>
 709        <FONT color="red">by induction on&#x00a0;</FONT>
 710        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
 711         <xsl:with-param name="current_indent" select="$current_indent+30"/>
 712        </xsl:apply-templates>
 713        <!--
 714        <br/>
 715        <xsl:call-template name="make_indent">
 716         <xsl:with-param name="current_indent" select="$current_indent"/>
 717        </xsl:call-template>
 718        <xsl:text>The induction property is</xsl:text>
 719        <br/>
 720        <xsl:call-template name="make_indent">
 721         <xsl:with-param name="current_indent" select="$current_indent"/>
 722        </xsl:call-template>
 723        <xsl:apply-templates select="*[3]">
 724         <xsl:with-param name="current_indent" select="$current_indent"/>
 725        </xsl:apply-templates>
 726        -->
 727        <xsl:apply-templates
 728             select="*[position()>3 and not(position()=last())]">
 729         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 730        </xsl:apply-templates>
 731        <!-- <br/>
 732        <xsl:call-template name="make_indent">
 733         <xsl:with-param name="current_indent" select="$current_indent"/>
 734        </xsl:call-template>
 735        <xsl:text>End induction</xsl:text> -->
 736       </xsl:when>
 737       <!-- inductive_case -->
 738       <xsl:when test="$name='inductive_case'">
 739        <br/>
 740        <xsl:call-template name="make_indent">
 741         <xsl:with-param name="current_indent" select="$current_indent"/>
 742        </xsl:call-template>
 743        <FONT color="red">Case&#x00a0;</FONT>
 744        <xsl:apply-templates select="*[2]">
 745         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 746        </xsl:apply-templates>
 747        <xsl:if test="*[3]/*[position()>1]">
 748         <br/>
 749         <xsl:call-template name="make_indent">
 750          <xsl:with-param name="current_indent" select="$current_indent+4"/>
 751         </xsl:call-template>
 752         <FONT color="red">By induction hypothesis, we have:</FONT>
 753         <xsl:for-each select="*[3]/*[position()>1]">
 754          <br/>
 755          <xsl:call-template name="make_indent">
 756           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 757          </xsl:call-template>
 758          <xsl:text>(</xsl:text>
 759          <xsl:apply-templates select="m:ci"/>
 760          <xsl:text>)&#x00a0;</xsl:text>
 761          <xsl:apply-templates select="m:type">
 762           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 763          </xsl:apply-templates>
 764         </xsl:for-each>
 765        </xsl:if>
 766        <br/>
 767         <xsl:call-template name="make_indent">
 768          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 769         </xsl:call-template>
 770        <xsl:apply-templates select="*[4]">
 771         <xsl:with-param name="current_indent" select="$current_indent +4"/>
 772        </xsl:apply-templates>
 773        <!-- <br/>
 774        <xsl:call-template name="make_indent">
 775         <xsl:with-param name="current_indent" select="$current_indent"/>
 776        </xsl:call-template>
 777        <xsl:text>End Case</xsl:text> -->
 778       </xsl:when>
 779       <!-- case_lhs  -->
 780       <xsl:when test="$name='case_lhs'">
 781        <xsl:choose>
 782         <xsl:when test="count(*)=2">
 783          <xsl:apply-templates mode="inline" select="*[2]"/>
 784         </xsl:when>
 785         <xsl:otherwise>
 786          <xsl:text>(</xsl:text>
 787          <xsl:apply-templates mode="inline" select="*[2]"/>
 788          <xsl:for-each select="m:bvar">
 789           <xsl:text>&#x00a0;</xsl:text>
 790           <xsl:apply-templates mode="inline" select="*[1]"/>
 791           <xsl:text>:</xsl:text>
 792           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
 793          </xsl:for-each>
 794          <xsl:text>)</xsl:text>
 795         </xsl:otherwise>
 796        </xsl:choose>
 797       </xsl:when>
 798       <!-- nat_ind -->
 799       <xsl:when test="$name='nat_ind_complete'">
 800        <FONT color="red">By induction on&#x00a0;</FONT>
 801        <xsl:apply-templates select="*[2]"/>:
 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>0&#x00a0;</xsl:text>
 807        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 808        <xsl:apply-templates select="*[3]">
 809         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 810        </xsl:apply-templates>
 811        <br/>
 812        <xsl:call-template name="make_indent">
 813         <xsl:with-param name="current_indent" select="$current_indent"/>
 814        </xsl:call-template>
 815        <xsl:text>S(</xsl:text>
 816        <xsl:apply-templates select="*[4]"/>
 817        <xsl:text>)&#x00a0;</xsl:text>
 818        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 819        <FONT color="red">Assume by induction</FONT>
 820        <br/>
 821        <xsl:call-template name="make_indent">
 822         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 823        </xsl:call-template>
 824        <xsl:text>(</xsl:text>
 825        <xsl:apply-templates select="*[5]"/>
 826        <xsl:text>)</xsl:text>
 827        <xsl:apply-templates select="*[6]">
 828         <xsl:with-param name="current_indent" select="$current_indent + 14"/>
 829        </xsl:apply-templates>
 830        <br/>
 831        <xsl:call-template name="make_indent">
 832         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 833        </xsl:call-template>
 834        <xsl:apply-templates select="*[7]">
 835         <xsl:with-param name="current_indent" select="$current_indent + 10"/>
 836        </xsl:apply-templates>
 837       </xsl:when>
 838       <!-- false_ind -->
 839       <xsl:when test="$name='false_ind'">
 840        <xsl:apply-templates select="*[3]">
 841         <xsl:with-param name="current_indent" select="$current_indent"/>
 842        </xsl:apply-templates>
 843        <br/>
 844        <xsl:call-template name="make_indent">
 845         <xsl:with-param name="current_indent" select="$current_indent"/>
 846        </xsl:call-template>
 847        <FONT color="red">Contradiction.</FONT>
 848       </xsl:when>
 849       <!-- and_ind -->
 850       <xsl:when test="$name='and_ind'">
 851        <xsl:choose>
 852         <xsl:when test="name(*[2])='m:apply'">
 853          <xsl:apply-templates select="*[2]">
 854           <xsl:with-param name="current_indent" select="$current_indent"/>
 855          </xsl:apply-templates>
 856         </xsl:when>
 857         <xsl:otherwise>
 858          <FONT color="red">Consider&#x00a0;</FONT>
 859          <xsl:apply-templates select="*[2]"/>
 860         </xsl:otherwise>
 861        </xsl:choose>
 862        <br/>
 863        <xsl:call-template name="make_indent">
 864         <xsl:with-param name="current_indent" select="$current_indent"/>
 865        </xsl:call-template>
 866        <FONT color="red">In particular, we have</FONT>
 867        <br/>
 868        <xsl:call-template name="make_indent">
 869         <xsl:with-param name="current_indent" select="$current_indent"/>
 870        </xsl:call-template>
 871        (
 872        <xsl:apply-templates select="*[3]"/>
 873        )&#x00a0;
 874        <xsl:apply-templates select="*[4]">
 875         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 876        </xsl:apply-templates>
 877        <br/>
 878        <xsl:call-template name="make_indent">
 879         <xsl:with-param name="current_indent" select="$current_indent"/>
 880        </xsl:call-template>
 881        (
 882        <xsl:apply-templates select="*[5]"/>
 883        )&#x00a0;
 884        <xsl:apply-templates select="*[6]">
 885         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
 886        </xsl:apply-templates>
 887        <br/>
 888        <xsl:call-template name="make_indent">
 889         <xsl:with-param name="current_indent" select="$current_indent"/>
 890        </xsl:call-template>
 891        <xsl:apply-templates select="*[7]">
 892         <xsl:with-param name="current_indent" select="$current_indent"/>
 893        </xsl:apply-templates>
 894       </xsl:when>
 895       <!-- full_or_ind -->
 896       <xsl:when test="$name='full_or_ind'">
 897        <xsl:choose>
 898         <xsl:when test="name(*[2])='m:apply'">
 899          <xsl:apply-templates select="*[2]">
 900           <xsl:with-param name="current_indent" select="$current_indent"/>
 901          </xsl:apply-templates>
 902         </xsl:when>
 903         <xsl:otherwise>
 904          <FONT color="red">Consider&#x00a0;</FONT>
 905          <xsl:apply-templates select="*[2]"/>
 906         </xsl:otherwise>
 907        </xsl:choose>
 908        <br/>
 909        <xsl:call-template name="make_indent">
 910         <xsl:with-param name="current_indent" select="$current_indent"/>
 911        </xsl:call-template>
 912        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
 913        <xsl:apply-templates select="*[3]"/>
 914        <br/>
 915        <xsl:call-template name="make_indent">
 916         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 917        </xsl:call-template>
 918        <FONT color="red">Left: suppose&#x00a0;</FONT>
 919        <xsl:text>(</xsl:text>
 920        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
 921        <xsl:text>)&#x00a0;</xsl:text>
 922        <xsl:apply-templates
 923             select="*[4]/m:bvar/m:type/*[1]"/>
 924        <br/>
 925        <xsl:call-template name="make_indent">
 926         <xsl:with-param name="current_indent" select="$current_indent+15"/>
 927        </xsl:call-template>
 928        <xsl:apply-templates
 929             select="*[4]/*[3]">
 930         <xsl:with-param name="current_indent" select="$current_indent+15"/>
 931        </xsl:apply-templates>
 932        <br/>
 933        <xsl:call-template name="make_indent">
 934         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 935        </xsl:call-template>
 936        <FONT color="red">Right: suppose&#x00a0;</FONT>
 937        <xsl:text>(</xsl:text>
 938        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
 939        <xsl:text>)&#x00a0;</xsl:text>
 940        <xsl:apply-templates
 941             select="*[5]/m:bvar/m:type/*[1]"/>
 942        <br/>
 943        <xsl:call-template name="make_indent">
 944         <xsl:with-param name="current_indent" select="$current_indent+16"/>
 945        </xsl:call-template>
 946        <xsl:apply-templates
 947             select="*[5]/*[3]">
 948         <xsl:with-param name="current_indent" select="$current_indent+16"/>
 949        </xsl:apply-templates>
 950       </xsl:when>
 951       <!-- or_ind -->
 952       <xsl:when test="$name='or_ind'">
 953        <xsl:choose>
 954         <xsl:when test="name(*[2])='m:apply'">
 955          <xsl:apply-templates select="*[2]">
 956           <xsl:with-param name="current_indent" select="$current_indent"/>
 957          </xsl:apply-templates>
 958         </xsl:when>
 959         <xsl:otherwise>
 960          <FONT color="red">Consider&#x00a0;</FONT>
 961          <xsl:apply-templates select="*[2]"/>
 962         </xsl:otherwise>
 963        </xsl:choose>
 964        <br/>
 965        <xsl:call-template name="make_indent">
 966         <xsl:with-param name="current_indent" select="$current_indent"/>
 967        </xsl:call-template>
 968        <FONT color="red">We prove&#x00a0;</FONT>
 969        <xsl:apply-templates select="*[3]"/>
 970        <FONT color="red">&#x00a0;by cases:</FONT>
 971        <br/>
 972        <xsl:call-template name="make_indent">
 973         <xsl:with-param name="current_indent" select="$current_indent"/>
 974        </xsl:call-template>
 975        *
 976        <xsl:apply-templates select="*[4]">
 977         <xsl:with-param name="current_indent" select="$current_indent"/>
 978        </xsl:apply-templates>
 979        <br/>
 980        <xsl:call-template name="make_indent">
 981         <xsl:with-param name="current_indent" select="$current_indent"/>
 982        </xsl:call-template>
 983        *
 984        <xsl:apply-templates select="*[5]">
 985         <xsl:with-param name="current_indent" select="$current_indent"/>
 986        </xsl:apply-templates>
 987       </xsl:when>
 988       <!-- Ex_ind -->
 989       <xsl:when test="$name='ex_ind'">
 990        <xsl:choose>
 991         <xsl:when test="name(*[2])='m:apply'">
 992          <xsl:apply-templates select="*[2]">
 993           <xsl:with-param name="current_indent" select="$current_indent"/>
 994          </xsl:apply-templates>
 995         </xsl:when>
 996         <xsl:otherwise>
 997          <FONT color="red">Consider&#x00a0;</FONT>
 998          <xsl:apply-templates select="*[2]">
 999           <xsl:with-param name="current_indent" select="$current_indent"/>
1000          </xsl:apply-templates>
1001         </xsl:otherwise>
1002        </xsl:choose>
1003        <br/>
1004        <xsl:call-template name="make_indent">
1005         <xsl:with-param name="current_indent" select="$current_indent"/>
1006        </xsl:call-template>
1007        <FONT color="red">Let&#x00a0;</FONT>
1008        <xsl:apply-templates mode="inline" select="*[3]"/>
1009        :
1010        <xsl:apply-templates mode="inline" select="*[4]"/>
1011        <FONT color="red">&#x00a0;such that</FONT>
1012        <br/>
1013        <xsl:call-template name="make_indent">
1014         <xsl:with-param name="current_indent" select="$current_indent"/>
1015        </xsl:call-template>
1016        (
1017        <xsl:apply-templates mode="inline" select="*[5]"/>
1018        )
1019        <xsl:apply-templates select="*[6]">
1020         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1021        </xsl:apply-templates>
1022        <br/>
1023        <xsl:call-template name="make_indent">
1024         <xsl:with-param name="current_indent" select="$current_indent"/>
1025        </xsl:call-template>
1026        <xsl:apply-templates select="*[7]">
1027         <xsl:with-param name="current_indent" select="$current_indent"/>
1028        </xsl:apply-templates>
1029       </xsl:when>
1030
1031       <!-- INTERP -->
1032       <xsl:when test="$name='interp'">
1033          <font color="green">[</font>
1034             <xsl:apply-templates select="*[2]"/>
1035          <font color="green">]</font>
1036       </xsl:when>
1037
1038      </xsl:choose>
1039 </xsl:template>
1040
1041 <!-- LAMBDA -->
1042
1043 <xsl:template match="m:lambda">
1044 <xsl:param name="current_indent" select="0"/>
1045     <xsl:variable name="charlength">
1046      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1047      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1048     </xsl:variable>
1049     <!-- <xsl:value-of select="$charlength"/> -->
1050     <!-- <xsl:value-of select="$current_indent"/> -->
1051      <xsl:choose>
1052      <xsl:when test="$charlength > $framewidth">
1053        <!-- &#x03bb; -->
1054        <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
1055        <xsl:apply-templates select="m:bvar/m:ci"/>
1056        <xsl:text>:</xsl:text>
1057        <xsl:apply-templates select="m:bvar/m:type">
1058         <xsl:with-param name="current_indent"
1059            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1060        </xsl:apply-templates><br/>
1061        <xsl:call-template name="make_indent">
1062         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1063        </xsl:call-template>
1064        <xsl:text>.</xsl:text>
1065        <xsl:apply-templates select="*[position()=2]">
1066         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1067        </xsl:apply-templates>
1068      </xsl:when>
1069      <xsl:otherwise>
1070       <xsl:apply-templates mode="inline" select="."/>
1071      </xsl:otherwise>
1072      </xsl:choose>
1073 </xsl:template>
1074
1075 <!-- href -->
1076 <xsl:template match="m:ci">
1077  <xsl:choose>
1078   <xsl:when test="boolean(@definitionURL)">
1079    <a href="{@definitionURL}">
1080    <xsl:apply-templates/>
1081    </a>
1082   </xsl:when>
1083   <xsl:otherwise>
1084    <xsl:value-of select="."/>
1085   </xsl:otherwise>
1086  </xsl:choose>
1087 </xsl:template>
1088
1089 <!-- COUNTING -->
1090
1091 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1092 <xsl:param name="incurrent_length" select="0"/>
1093     <xsl:choose>
1094     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1095      <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>
1096      <xsl:choose>
1097      <xsl:when test="string($siblength) = &quot;&quot;">
1098       <xsl:value-of select="$incurrent_length + string-length()"/>
1099      </xsl:when>
1100      <xsl:otherwise>
1101       <xsl:value-of select="number($siblength)"/>
1102      </xsl:otherwise>
1103      </xsl:choose>
1104     </xsl:when>
1105     <xsl:otherwise>
1106      <xsl:value-of select="$incurrent_length + string-length()"/>
1107     </xsl:otherwise>
1108     </xsl:choose>
1109 </xsl:template>
1110
1111 <xsl:template match="*" mode="charcount">
1112  <xsl:param name="incurrent_length" select="0"/>
1113  <xsl:choose>
1114   <xsl:when test="count(child::*) = 0">
1115    <xsl:value-of select="$incurrent_length"/>
1116   </xsl:when>
1117   <xsl:otherwise>
1118     <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>
1119     <xsl:choose>
1120      <xsl:when test="$framewidth >= number($childlength)">
1121       <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>
1122       <xsl:choose>
1123        <xsl:when test="string($siblength) = &quot;&quot;">
1124         <xsl:value-of select="number($childlength)"/>
1125        </xsl:when>
1126        <xsl:otherwise>
1127         <xsl:value-of select="number($siblength)"/>
1128        </xsl:otherwise>
1129       </xsl:choose>
1130      </xsl:when>
1131      <xsl:otherwise>
1132       <xsl:value-of select="number($childlength)"/>
1133      </xsl:otherwise>
1134     </xsl:choose>
1135   </xsl:otherwise>
1136  </xsl:choose>
1137 </xsl:template>
1138
1139
1140 <!--***********************************************************************-->
1141 <!-- OBJECTS                                                               -->
1142 <!--***********************************************************************-->
1143
1144 <!-- DEFINITION -->
1145
1146 <xsl:template match="Definition">
1147 <xsl:param name="current_indent" select="0"/>
1148 <p>
1149 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1150 TYPE =<br/>
1151       <xsl:call-template name="make_indent">
1152        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1153       </xsl:call-template>
1154        <xsl:apply-templates select="type/*[1]">
1155         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1156        </xsl:apply-templates><br/>
1157 BODY =<br/>
1158       <xsl:call-template name="make_indent">
1159        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1160       </xsl:call-template>
1161        <xsl:apply-templates select="body/*[1]">
1162         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1163        </xsl:apply-templates>
1164 </p>
1165 </xsl:template>
1166
1167 <!-- AXIOM -->
1168
1169 <xsl:template match="Axiom">
1170 <xsl:param name="current_indent" select="0"/>
1171 <p>
1172 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1173 TYPE =<br/>
1174       <xsl:call-template name="make_indent">
1175        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1176       </xsl:call-template>
1177 <xsl:apply-templates select="type/*[1]">
1178           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1179        </xsl:apply-templates>
1180 </p>
1181 </xsl:template>
1182
1183 <!-- UNFINISHED PROOF -->
1184
1185 <xsl:template match="CurrentProof">
1186 <xsl:param name="current_indent" select="0"/>
1187 <p>
1188 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1189 THESIS:  <xsl:apply-templates select="type/*[1]">
1190           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1191          </xsl:apply-templates><br/>
1192 CONJECTURES:
1193       <xsl:for-each select="Conjecture">
1194       <br/>
1195       <xsl:call-template name="make_indent">
1196        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1197       </xsl:call-template>
1198       <xsl:value-of select="./@no"/> :
1199       <xsl:apply-templates select="./*[1]">
1200        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
1201       </xsl:apply-templates>
1202       </xsl:for-each>
1203       <br/>
1204 PROOF:
1205       <xsl:apply-templates select="body/*[1]">
1206         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1207       </xsl:apply-templates>
1208 </p>
1209 </xsl:template>
1210
1211 <!-- MUTUAL INDUCTIVE DEFINITION -->
1212
1213 <xsl:template match="InductiveDefinition">
1214 <xsl:param name="current_indent" select="0"/>
1215 <p>
1216      <xsl:for-each select="InductiveType">
1217          <xsl:choose>
1218          <xsl:when test="position() = 1">
1219           <xsl:choose>
1220           <xsl:when test="string(./@inductive) = &quot;true&quot;">
1221           INDUCTIVE DEFINITION
1222           </xsl:when>
1223           <xsl:otherwise>
1224           COINDUCTIVE DEFINITION
1225           </xsl:otherwise>
1226           </xsl:choose>
1227          </xsl:when>
1228          <xsl:otherwise>
1229           AND
1230          </xsl:otherwise>
1231          </xsl:choose>
1232          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
1233          [
1234           <xsl:if test="string(../Param) != &quot;&quot;">
1235            <xsl:for-each select="../Param">
1236             <xsl:value-of select="./@name"/>
1237             :
1238             <xsl:apply-templates select="*"/>
1239            </xsl:for-each>
1240           </xsl:if>
1241          ] <br/>
1242          OF ARITY
1243          <xsl:apply-templates select="./arity/*[1]">
1244           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1245          </xsl:apply-templates> <br/>
1246          BUILT FROM:
1247       <xsl:for-each select="./Constructor">
1248       <br/>
1249       <xsl:call-template name="make_indent">
1250        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1251       </xsl:call-template>
1252          <xsl:choose>
1253          <xsl:when test="position() = 1">
1254          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1255          </xsl:when>
1256          <xsl:otherwise>
1257          <xsl:text>| </xsl:text>
1258          </xsl:otherwise>
1259          </xsl:choose>
1260          <xsl:value-of select="./@name"/>
1261          <xsl:text>: </xsl:text>
1262          <xsl:apply-templates select="./*[1]">
1263           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1264          </xsl:apply-templates>
1265       </xsl:for-each>
1266      </xsl:for-each>
1267 </p>
1268 </xsl:template>
1269
1270 <!-- VARIABLE -->
1271
1272 <xsl:template match="Variable">
1273 <xsl:param name="current_indent" select="0"/>
1274 <p>
1275 VARIABLE <xsl:value-of select="@name"/><br/>
1276 TYPE = <xsl:apply-templates select="type/*[1]">
1277           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1278        </xsl:apply-templates>
1279 </p>
1280 </xsl:template>
1281
1282 <!--***********************************************************************-->
1283 <!-- SECTIONS                                                              -->
1284 <!--***********************************************************************-->
1285
1286 <!-- SECTION -->
1287
1288 <xsl:template match="SECTION">
1289 <xsl:param name="current_indent" select="0"/>
1290  <h1>BEGIN OF SECTION</h1>
1291   <xsl:apply-templates/>
1292  <h1>END OF SECTION</h1>
1293 </xsl:template>
1294
1295 </xsl:stylesheet>