helm/nuprl_stylesheets/nuprl_content_to_html2.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
  29
  30 <!--***********************************************************************-->
  31 <!-- From MathML content to HTML                                           -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi               -->
  33 <!--***********************************************************************-->
  34
  35 <xsl:param name="CICURI" select="''"/>
  36 <xsl:param name="type" select="'standalone'"/>
  37 <xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
  38 <xsl:param name="explode_tactics" select="false()"/>
  39
  40 <xsl:include href="nuprl_html_arith.xsl"/>
  41 <xsl:include href="nuprl_html_basic.xsl"/>
  42
  43 <xsl:variable name="showcast" select="0"/>
  44
  45 <!--***********************************************************************-->
  46 <!-- HTML Head and Body                                                    -->
  47 <!--***********************************************************************-->
  48
  49 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
  50
  51 <!-- document needs method="xml" and searches locally for the dtd if        -->
  52 <!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
  53 <!-- For having output html must be media-type="html" and for having the    -->
  54 <!-- correct <br /> you must specify at least the remote dtd by means of    -->
  55 <!-- doctype-public                                                         -->
  56
  57 <!-- Commentd out by Zack, a try-fix for NuPRL stylesheets with OCaml UWOBO -->
  58 <!--
  59 <xsl:output
  60         method="xml"
  61         encoding="iso-8859-1"
  62         media-type="text/html"
  63         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  64 -->
  65 <xsl:output
  66         method="html"
  67         encoding="iso-8859-1"
  68         media-type="text/html"
  69         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  70
  71 <xsl:variable name="framewidth" select="55"/>
  72
  73 <!--forall-->
  74   <xsl:variable name="forall">
  75     <xsl:choose>
  76       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&quot;</xsl:when>
  77       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2200;</xsl:when>
  78       <xsl:otherwise>???</xsl:otherwise>
  79     </xsl:choose>
  80   </xsl:variable>
  81 <!--lambda-->
  82   <xsl:variable name="lambda">
  83     <xsl:choose>
  84       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">l</xsl:when>
  85       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3BB;</xsl:when>
  86       <xsl:otherwise>???</xsl:otherwise>
  87     </xsl:choose>
  88   </xsl:variable>
  89 <!--prod-->
  90   <xsl:variable name="prod">
  91     <xsl:choose>
  92       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xD5;</xsl:when>
  93       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3A0;</xsl:when>
  94       <xsl:otherwise>???</xsl:otherwise>
  95     </xsl:choose>
  96   </xsl:variable>
  97 <!--arrow-->
  98   <xsl:variable name="arrow">
  99     <xsl:choose>
 100       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xAE;</xsl:when>
 101       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2192;</xsl:when>
 102       <xsl:otherwise>???</xsl:otherwise>
 103     </xsl:choose>
 104   </xsl:variable>
 105 <!--RightArrow-->
 106   <xsl:variable name="RightArrow">
 107     <xsl:choose>
 108       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xDE;</xsl:when>
 109       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x21D2;</xsl:when>
 110       <xsl:otherwise>???</xsl:otherwise>
 111     </xsl:choose>
 112   </xsl:variable>
 113 <!--product-->
 114   <xsl:variable name="product">
 115     <xsl:choose>
 116       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">S</xsl:when>
 117       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#931;</xsl:when>
 118       <xsl:otherwise>???</xsl:otherwise>
 119     </xsl:choose>
 120   </xsl:variable>
 121 <!--member-->
 122   <xsl:variable name="member">
 123     <xsl:choose>
 124       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xce;</xsl:when>
 125       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8712;</xsl:when>
 126       <xsl:otherwise>???</xsl:otherwise>
 127     </xsl:choose>
 128   </xsl:variable>
 129 <!--member-->
 130   <xsl:variable name="intersection">
 131     <xsl:choose>
 132       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xc7;</xsl:when>
 133       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8745;</xsl:when>
 134       <xsl:otherwise>???</xsl:otherwise>
 135     </xsl:choose>
 136   </xsl:variable>
 137 <!--integers-->
 138   <xsl:variable name="integers">
 139     <xsl:choose>
 140       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">I</xsl:when>
 141       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#921;</xsl:when>
 142       <xsl:otherwise>???</xsl:otherwise>
 143     </xsl:choose>
 144   </xsl:variable>
 145 <!--naturalnumbers-->
 146   <xsl:variable name="naturalnumbers">
 147     <xsl:choose>
 148       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">N</xsl:when>
 149       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#925;</xsl:when>
 150       <xsl:otherwise>???</xsl:otherwise>
 151     </xsl:choose>
 152   </xsl:variable>
 153 <!--implies-->
 154   <xsl:variable name="implies">
 155     <xsl:choose>
 156       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xee;</xsl:when>
 157       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8658;</xsl:when>
 158       <xsl:otherwise>???</xsl:otherwise>
 159     </xsl:choose>
 160   </xsl:variable>
 161 <!--exists-->
 162   <xsl:variable name="NUPRLexists">
 163     <xsl:choose>
 164       <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#x24;</xsl:when>
 165       <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8707;</xsl:when>
 166       <xsl:otherwise>???</xsl:otherwise>
 167     </xsl:choose>
 168   </xsl:variable>
 169
 170
 171
 172 <xsl:template name="mksymbol">
 173         <xsl:param name="symbol" select="'???'"/>
 174         <xsl:param name="color"  select="'blue'"/>
 175         <xsl:param name="size"   select="''"/>
 176
 177         <xsl:choose>
 178                 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
 179                         <FONT FACE="symbol" SIZE="{$size}" COLOR="{$color}">
 180                                 <xsl:value-of select="$symbol"/>
 181                         </FONT>
 182                 </xsl:when>
 183                 <xsl:otherwise>
 184                         <FONT COLOR="{$color}">
 185                                 <xsl:value-of select="$symbol"/>
 186                         </FONT>
 187                 </xsl:otherwise>
 188         </xsl:choose>
 189 </xsl:template>
 190
 191 <xsl:template match="/">
 192  <xsl:param name="current_indent" select="0"/>
 193  <xsl:choose>
 194   <xsl:when test="$type = 'standalone'">
 195    <html>
 196       <head>
 197          <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
 198          <style> A { text-decoration: none } </style>
 199          <script>
 200           <xsl:text disable-output-escaping="yes">
 201            <![CDATA[
 202             function Hide(which){
 203              if (!document.getElementById)
 204               return
 205              which.style.display="none"
 206             }
 207
 208             function Show(which){
 209              if (!document.getElementById)
 210               return
 211              which.style.display=""
 212             }
 213
 214             document.to_be_deleted = new Array();
 215           ]]>
 216           </xsl:text>
 217          </script>
 218         </head>
 219       <body bgcolor="white">
 220          <xsl:attribute name="onLoad">
 221           if(document.getElementById)
 222            for(var i=0;i&lt;document.to_be_deleted.length;i++)
 223             Hide(document.getElementById(document.to_be_deleted[i]));
 224          </xsl:attribute>
 225          <xsl:apply-templates>
 226             <xsl:with-param name="current_indent" select="0"/>
 227          </xsl:apply-templates>
 228       </body>
 229    </html>
 230   </xsl:when>
 231   <xsl:otherwise>
 232    <to_be_embedded>
 233     <xsl:apply-templates>
 234      <xsl:with-param name="current_indent" select="0"/>
 235     </xsl:apply-templates>
 236    </to_be_embedded>
 237   </xsl:otherwise>
 238  </xsl:choose>
 239 </xsl:template>
 240
 241 <!--***********************************************************************-->
 242 <!-- Indentation                                                           -->
 243 <!--***********************************************************************-->
 244
 245 <xsl:template name="make_indent">
 246         <xsl:param name="current_indent" select="0"/>
 247         <xsl:if test="$current_indent > 0">
 248                 <xsl:text>&#x00a0;</xsl:text>
 249                 <xsl:call-template name="make_indent">
 250                 <xsl:with-param name="current_indent" select="$current_indent - 1"/>
 251                 </xsl:call-template>
 252         </xsl:if>
 253 </xsl:template>
 254
 255 <!-- Syntactic Sugar -->
 256 <xsl:template match="m:type">
 257 <xsl:param name="current_indent" select="0"/>
 258 <xsl:apply-templates>
 259  <xsl:with-param name="current_indent"
 260            select="$current_indent"/>
 261 </xsl:apply-templates>
 262 </xsl:template>
 263
 264 <xsl:template match="m:condition">
 265 <xsl:param name="current_indent" select="0"/>
 266 <xsl:apply-templates>
 267  <xsl:with-param name="current_indent"
 268            select="$current_indent"/>
 269 </xsl:apply-templates>
 270 </xsl:template>
 271
 272 <xsl:template match="m:math">
 273 <xsl:param name="current_indent" select="0"/>
 274 <xsl:apply-templates>
 275  <xsl:with-param name="current_indent"
 276            select="$current_indent"/>
 277 </xsl:apply-templates>
 278 </xsl:template>
 279
 280
 281
 282 <!--*********************************************************************-->
 283 <!--                         INLINE MODE                                 -->
 284 <!--*********************************************************************-->
 285
 286 <!-- href -->
 287 <xsl:template mode="inline" match="m:ci">
 288  <xsl:choose>
 289   <xsl:when test="boolean(@definitionURL)">
 290    <a href="{@definitionURL}">
 291    <xsl:apply-templates/>
 292    </a>
 293   </xsl:when>
 294   <xsl:otherwise>
 295    <xsl:value-of select="."/>
 296   </xsl:otherwise>
 297  </xsl:choose>
 298 </xsl:template>
 299
 300 <!-- CSYMBOL -->
 301
 302 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 303  <xsl:param name="current_indent" select="0"/>
 304    <xsl:variable name="name">
 305     <xsl:value-of select="m:csymbol"/>
 306    </xsl:variable>
 307    <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 308    <xsl:choose>
 309
 310     <!-- FUNCTION-DIP (PROD) -->
 311         <xsl:when test="$name='prod'">
 312                 <xsl:call-template name="mksymbol">
 313                         <xsl:with-param name="symbol" select="$prod"/>
 314                         <xsl:with-param name="color" select="'blue'"/>
 315                         <xsl:with-param name="size" select="'+2'"/>
 316                 </xsl:call-template>
 317                 <xsl:apply-templates select="m:bvar/m:ci"/>
 318                 <xsl:if test="m:bvar/m:ci=&quot;&quot;">
 319                         <xsl:text>""</xsl:text>
 320                 </xsl:if>
 321                 <xsl:text>:</xsl:text>
 322                 <!--<xsl:if test="m:bvar/m:type/*[*]">
 323                         <xsl:text>( </xsl:text>
 324                 </xsl:if>-->
 325                 <xsl:apply-templates select="m:bvar/m:type"/>
 326                 <!--<xsl:if test="m:bvar/m:type/*[*]">
 327                         <xsl:text>) </xsl:text>
 328                 </xsl:if>-->
 329                 <xsl:text>.</xsl:text>
 330                 <xsl:apply-templates select="*[position()=3]"/>
 331         </xsl:when>
 332
 333         <!-- ARROW --> <!-- FUNCTION (IND) -->
 334     <xsl:when test="$name='arrow'">
 335         <xsl:text>(</xsl:text>
 336         <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 337         <xsl:call-template name="mksymbol">
 338                 <xsl:with-param name="symbol" select="$arrow"/>
 339                 <xsl:with-param name="color" select="'blue'"/>
 340                 <xsl:with-param name="size" select="'+0'"/>
 341         </xsl:call-template>
 342         <xsl:apply-templates  select="*[position()=3]"/>
 343         <xsl:text>)</xsl:text>
 344     </xsl:when>
 345
 346
 347     <!-- FORALL -->
 348     <xsl:when test="$name='forall'">
 349         <xsl:call-template name="mksymbol">
 350                 <xsl:with-param name="symbol" select="$forall"/>
 351                 <xsl:with-param name="color" select="'blue'"/>
 352                 <xsl:with-param name="size" select="'+2'"/>
 353         </xsl:call-template>
 354         <xsl:apply-templates select="m:bvar/m:ci"/>
 355         <xsl:text>:</xsl:text>
 356         <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
 357                 <xsl:text>(</xsl:text>
 358         </xsl:if>-->
 359         <xsl:apply-templates select="m:bvar/m:type"/>
 360         <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
 361                 <xsl:text>)</xsl:text>
 362         </xsl:if>-->
 363         <xsl:text>.</xsl:text>
 364         <xsl:apply-templates select="*[position()=3]"/>
 365    </xsl:when>
 366
 367
 368     <!-- PRODUCT -->
 369     <xsl:when test="$name='product'">
 370         <xsl:call-template name="mksymbol">
 371                 <xsl:with-param name="symbol" select="$product"/>
 372                 <xsl:with-param name="color" select="'blue'"/>
 373                 <xsl:with-param name="size" select="'+2'"/>
 374         </xsl:call-template>
 375         <xsl:apply-templates select="m:bvar/m:ci"/>
 376         <xsl:text>:</xsl:text>
 377         <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 378         <xsl:text>.</xsl:text>
 379         <xsl:apply-templates select="*[position()=3]"/>
 380     </xsl:when>
 381
 382     <!-- PROD_IND -->
 383     <xsl:when test="$name='product_ind'">
 384      <FONT color="blue">
 385      <xsl:text>( </xsl:text>
 386      </FONT>
 387      <xsl:apply-templates mode="inline" select="m:type"/>
 388      <FONT color="blue" size="+2">
 389      <xsl:text>x</xsl:text>
 390      </FONT>
 391      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 392      <FONT color="blue">
 393      <xsl:text> )</xsl:text>
 394      </FONT>
 395
 396     </xsl:when>
 397
 398    <!-- PAIR -->
 399    <xsl:when test="$name='pair'">
 400         <FONT color="blue" size="+1">
 401         <xsl:text>&lt;</xsl:text>
 402         </FONT>
 403         <xsl:apply-templates select="*[2]"/>
 404         <xsl:text>, </xsl:text>
 405         <xsl:apply-templates select="*[3]"/>
 406         <FONT color="blue" size="+1">
 407         <xsl:text>&gt;</xsl:text>
 408         </FONT>
 409    </xsl:when>
 410
 411    <!-- UNION -->
 412    <xsl:when test="$name='union'">
 413         <xsl:apply-templates select="*[2]"/>
 414         <FONT color="blue" size="+2">
 415         <xsl:text>+</xsl:text>
 416         </FONT>
 417         <xsl:apply-templates select="*[3]"/>
 418   </xsl:when>
 419
 420   <!-- INL -->
 421   <xsl:when test="$name='inl'">
 422         <FONT color="blue">
 423         <xsl:text>inl (</xsl:text>
 424         </FONT>
 425         <xsl:apply-templates select="*[2]"/>
 426         <FONT color="blue">
 427         <xsl:text> )</xsl:text>
 428         </FONT>
 429   </xsl:when>
 430
 431    <!-- INR -->
 432   <xsl:when test="$name='inr'">
 433         <FONT color="blue" size="+1">
 434         <xsl:text>inr (</xsl:text>
 435         </FONT>
 436         <xsl:apply-templates select="*[2]"/>
 437         <FONT color="blue" size="+1">
 438         <xsl:text> )</xsl:text>
 439         </FONT>
 440   </xsl:when>
 441
 442         <!-- EQUAL -->
 443         <xsl:when test="$name='equal'">
 444                 <xsl:apply-templates select="*[position()=3]"/>
 445                 <FONT color="blue" size="+1">
 446                 <xsl:text> = </xsl:text>
 447                 </FONT>
 448                 <xsl:apply-templates select="*[position()=4]"/>
 449                 <xsl:text> </xsl:text>
 450                 <xsl:call-template name="mksymbol">
 451                 <xsl:with-param name="symbol" select="$member"/>
 452                 <xsl:with-param name="color" select="'blue'"/>
 453                 <xsl:with-param name="size" select="'+0'"/>
 454                 </xsl:call-template>
 455                 <xsl:text> </xsl:text>
 456                 <xsl:apply-templates select="*[position()=2]">
 457                  <xsl:with-param name="current_indent" select="$current_indent"/>
 458                 </xsl:apply-templates>
 459         </xsl:when>
 460
 461        <!-- CONS -->
 462         <xsl:when test="$name='cons'">
 463                 <xsl:apply-templates select="*[2]"/>
 464                 <FONT color="blue">
 465                 <xsl:text>::</xsl:text>
 466                 </FONT>
 467                 <xsl:apply-templates select="*[3]"/>
 468         </xsl:when>
 469
 470         <!-- REC -->
 471
 472         <xsl:when test="$name='rec'">
 473                 <FONT color="blue">
 474                 <xsl:text>rectype</xsl:text>
 475                 </FONT>
 476                 <xsl:apply-templates select="*[2]"/>
 477                 <FONT color="blue">
 478                 <xsl:text>=</xsl:text>
 479                 </FONT>
 480                 <xsl:apply-templates select="*[3]"/>
 481         </xsl:when>
 482
 483
 484         <!-- SET -->
 485
 486         <xsl:when test="$name='t_set'">
 487                 <FONT color="blue">
 488                 <xsl:text>{</xsl:text>
 489                 </FONT>
 490                 <xsl:choose>
 491                 <xsl:when test="m:bvar/m:ci">
 492                         <xsl:apply-templates select="m:bvar/m:ci"/>
 493                         <FONT color="blue">
 494                         <xsl:text>:</xsl:text>
 495                         </FONT>
 496                         <xsl:apply-templates select="m:bvar/m:type"/>
 497                 </xsl:when>
 498                 <xsl:otherwise>
 499                 <xsl:apply-templates select="m:bvar/m:type"/>
 500                 </xsl:otherwise>
 501                 </xsl:choose>
 502                 <FONT color="blue">
 503                 <xsl:text>|</xsl:text>
 504                 </FONT>
 505                 <xsl:apply-templates select="*[3]"/>
 506                 <FONT color="blue">
 507                         <xsl:text>}</xsl:text>
 508                 </FONT>
 509
 510         </xsl:when>
 511
 512         <!-- ISECT -->
 513
 514         <xsl:when test="$name='isect'">
 515                 <xsl:call-template name="mksymbol">
 516                 <xsl:with-param name="symbol" select="$intersection"/>
 517                 <xsl:with-param name="color" select="'blue'"/>
 518                 <xsl:with-param name="size" select="'+0'"/>
 519                 </xsl:call-template>
 520                 <xsl:apply-templates select="m:bvar/m:ci"/>
 521                 <FONT color="blue">
 522                 <xsl:text>:</xsl:text>
 523                 </FONT>
 524                 <xsl:apply-templates select="m:bvar/m:type"/>
 525                 <FONT color="blue">
 526                 <xsl:text>.</xsl:text>
 527                 </FONT>
 528                 <xsl:apply-templates select="*[3]"/>
 529         </xsl:when>
 530
 531         <!-- QUOTIENT -->
 532
 533         <xsl:when test="$name='quotient'">
 534                 <xsl:apply-templates select="m:bvar[1]"/>
 535                 <xsl:text>,</xsl:text>
 536                 <xsl:apply-templates select="m:bvar[2]"/>
 537                 <FONT color="blue">
 538                 <xsl:text>:</xsl:text>
 539                 </FONT>
 540                 <xsl:apply-templates select="*[2]"/>
 541                 <FONT color="blue">
 542                 <xsl:text>//</xsl:text>
 543                 </FONT>
 544                 <xsl:apply-templates select="*[5]"/>
 545         </xsl:when>
 546
 547         <!-- SO_LAMBDA -->
 548         <xsl:when test="$name='so_lambda'">
 549                         <xsl:call-template name="mksymbol">
 550                                 <xsl:with-param name="symbol" select="$lambda"/>
 551                                 <xsl:with-param name="color" select="'red'"/>
 552                                 <xsl:with-param name="size" select="'+2'"/>
 553                         </xsl:call-template>
 554                         <xsl:apply-templates select="m:apply[1]/*[2]"/>
 555                         <xsl:text>.</xsl:text>
 556                         <xsl:apply-templates select="*[3]"/>
 557      </xsl:when>
 558
 559
 560         <!-- SO_APPLY -->
 561
 562         <xsl:when test="$name='so_apply'">
 563                 <xsl:text>(</xsl:text>
 564                 <xsl:apply-templates select="*[position()=2]"/>
 565                 <xsl:for-each select="*[position()>2]">
 566                         <xsl:text>&#x00A0;</xsl:text>
 567                         <xsl:apply-templates mode="inline" select="."/>
 568                 </xsl:for-each>
 569                 <xsl:text>)</xsl:text>
 570       </xsl:when>
 571    <!-- APP -->
 572     <xsl:when test="$name='app'">
 573      <!-- NuPRL rendering -->
 574      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 575      <xsl:if test="count(*) &gt; 2">
 576       <xsl:text>(</xsl:text>
 577       <xsl:for-each select="*[position() &gt; 2]">
 578        <xsl:apply-templates select="." mode="inline"/>
 579        <xsl:if test="not(position() = last())">
 580         <xsl:text>,</xsl:text>
 581        </xsl:if>
 582       </xsl:for-each>
 583       <xsl:text>)</xsl:text>
 584      </xsl:if>
 585      <!-- CIC rendering
 586      <xsl:text>(</xsl:text>
 587      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 588      <xsl:for-each select="*[position()>2]">
 589       <xsl:text>&#x00A0;</xsl:text>
 590       <xsl:apply-templates mode="inline" select="."/>
 591      </xsl:for-each>
 592      <xsl:text>)</xsl:text>
 593      -->
 594     </xsl:when>
 595     <!-- CAST -->
 596     <xsl:when test="$name='cast'">
 597      <xsl:text>(</xsl:text>
 598      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 599      <xsl:text>:></xsl:text>
 600      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 601      <xsl:text>)</xsl:text>
 602     </xsl:when>
 603     <xsl:when test="$name='Prop'">
 604      <FONT color="violet">Prop</FONT>
 605     </xsl:when>
 606     <xsl:when test="$name='Set'">
 607      <FONT color="violet">Set</FONT>
 608     </xsl:when>
 609     <xsl:when test="$name='Type'">
 610      <FONT color="violet">Type</FONT>
 611     </xsl:when>
 612
 613    <!-- MUTCASE -->
 614     <xsl:when test="$name='mutcase'">
 615      <xsl:text>&lt;</xsl:text>
 616      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 617      <xsl:text>&gt; </xsl:text>
 618      <FONT color="red">CASE </FONT>
 619      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 620      <FONT color="red"> OF </FONT>
 621 <xsl:for-each select="m:piecewise/m:piece">
 622 <!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
 623       <xsl:choose>
 624        <xsl:when test="not(position() = 1)">
 625         <xsl:text> | </xsl:text>
 626        </xsl:when>
 627       </xsl:choose>
 628 <xsl:apply-templates mode="inline" select="./*[2]"/>
 629       <xsl:call-template name="mksymbol">
 630        <xsl:with-param name="symbol" select="$RightArrow"/>
 631        <xsl:with-param name="color" select="'green'"/>
 632        <xsl:with-param name="size" select="'+0'"/>
 633       </xsl:call-template>
 634       <xsl:apply-templates mode="inline"
 635            select="./*[1]"/>
 636      </xsl:for-each>
 637     </xsl:when>
 638
 639    <!-- FIX -->
 640     <xsl:when test="$name='fix'">
 641      <FONT color="red">FIX</FONT>
 642      <xsl:value-of select="m:ci"/>
 643      <xsl:text>{</xsl:text>
 644      <xsl:for-each select="m:bvar">
 645       <xsl:value-of select="m:ci"/>
 646       <xsl:text>:</xsl:text>
 647       <xsl:apply-templates mode="inline" select="m:type"/>
 648       <xsl:text>:=</xsl:text>
 649       <xsl:apply-templates mode="inline"
 650              select="following-sibling::*[position() = 1]"/>
 651       <xsl:choose>
 652        <xsl:when test="position()=last()">
 653         <xsl:text>}</xsl:text>
 654        </xsl:when>
 655        <xsl:otherwise>
 656         <xsl:text>;</xsl:text>
 657        </xsl:otherwise>
 658       </xsl:choose>
 659      </xsl:for-each>
 660     </xsl:when>
 661
 662    <!-- COFIX -->
 663     <xsl:when test="$name='cofix'">
 664      <xsl:text>COFIX</xsl:text>
 665      <xsl:value-of select="m:ci"/>
 666      <xsl:text>{</xsl:text>
 667      <xsl:for-each select="m:bvar">
 668       <xsl:value-of select="m:ci"/>
 669       <xsl:text>:</xsl:text>
 670       <xsl:apply-templates mode="inline" select="m:type"/>
 671       <xsl:text>:=</xsl:text>
 672       <xsl:apply-templates mode="inline"
 673           select="following-sibling::*[position() = 1]"/>
 674       <xsl:choose>
 675        <xsl:when test="position()=last()">
 676         <xsl:text>}</xsl:text>
 677        </xsl:when>
 678        <xsl:otherwise>
 679         <xsl:text>;</xsl:text>
 680        </xsl:otherwise>
 681       </xsl:choose>
 682      </xsl:for-each>
 683     </xsl:when>
 684
 685    <!-- proof -->
 686     <xsl:when test="$name='proof' or $name='side_proof'">
 687        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 688        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 689        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 690     </xsl:when>
 691     <xsl:when test="$name='letin1'">
 692      <xsl:text>letin1 (inline error)</xsl:text>
 693     </xsl:when>
 694     <!-- false_ind -->
 695     <xsl:when test="$name='false_ind'">
 696     <xsl:apply-templates mode="inline" select="*[3]"/>
 697     <FONT color="red">Contradiction.</FONT>
 698     </xsl:when>
 699     <!-- and_ind -->
 700     <xsl:when test="$name='and_ind'">
 701      <FONT color="red">From&#x00a0;</FONT>
 702      <xsl:apply-templates select="*[2]"/>
 703      <FONT color="red">&#x00a0;we get</FONT>
 704      (
 705      <xsl:apply-templates select="*[3]"/>
 706      )&#x00a0;
 707      <xsl:apply-templates mode="inline" select="*[4]"/>
 708      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 709      (
 710      <xsl:apply-templates select="*[5]"/>
 711      )&#x00a0;
 712      <xsl:apply-templates mode="inline" select="*[6]"/>
 713      ;
 714      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 715      <xsl:apply-templates mode="inline" select="*[7]"/>
 716     </xsl:when>
 717    </xsl:choose>
 718 </xsl:template>
 719
 720 <xsl:template mode="inline" match="m:lambda">
 721         <xsl:call-template name="mksymbol">
 722                 <xsl:with-param name="symbol" select="$lambda"/>
 723                 <xsl:with-param name="color" select="'red'"/>
 724                 <xsl:with-param name="size" select="'+2'"/>
 725         </xsl:call-template>
 726
 727       <!-- IN NuPrl non e' specificato il tipo -->
 728         <xsl:apply-templates select="m:bvar/m:ci"/>
 729         <xsl:if test="m:bvar[m:mtype]">
 730                 <xsl:text>:</xsl:text>
 731                 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 732         </xsl:if>
 733         <xsl:text>.</xsl:text>
 734       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 735 </xsl:template>
 736
 737 <!--*********************************************************************-->
 738 <!--                       NORMAL MODE                                   -->
 739 <!--*********************************************************************-->
 740
 741 <xsl:template match="m:apply[m:csymbol]">
 742     <xsl:param name="current_indent" select="0"/>
 743     <xsl:param name="width" select="$framewidth"/>
 744     <xsl:variable name="name">
 745      <xsl:value-of select="m:csymbol"/>
 746     </xsl:variable>
 747     <xsl:variable name="charlength">
 748      <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 749     </xsl:variable>
 750     <xsl:variable name="uri">
 751      <xsl:value-of select="*[1]/@definitionURL"/>
 752     </xsl:variable>
 753
 754
 755      <xsl:choose>
 756
 757      <!-- FUNCTION-DIP (PROD) -->
 758      <xsl:when test="$name='prod'">
 759        <xsl:choose>
 760                 <xsl:when test="$charlength > $framewidth">
 761                         <xsl:call-template name="mksymbol">
 762                                 <xsl:with-param name="symbol" select="$prod"/>
 763                                 <xsl:with-param name="color" select="'blue'"/>
 764                                 <xsl:with-param name="size" select="'+2'"/>
 765                         </xsl:call-template>
 766                         <xsl:apply-templates select="m:bvar/m:ci">
 767                         <xsl:with-param name="current_indent" select="$current_indent"/>
 768                         </xsl:apply-templates>
 769                         <xsl:if test="m:bvar/m:ci=&quot;&quot;">
 770                                 <xsl:text>""</xsl:text>
 771                         </xsl:if>
 772                         <xsl:text>:</xsl:text>
 773                         <!--<xsl:if test="m:bvar/m:type/*[*]">
 774                                 <xsl:text>( </xsl:text>
 775                         </xsl:if>-->
 776                         <xsl:apply-templates select="m:bvar/m:type">
 777                                 <xsl:with-param name="current_indent"
 778                                 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 779                         </xsl:apply-templates>
 780                         <!--<xsl:if test="m:bvar/m:type/*[*]">
 781                                 <xsl:text>) </xsl:text>
 782                         </xsl:if>-->
 783                         <br/>
 784                         <xsl:call-template name="make_indent">
 785                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 786                         </xsl:call-template>
 787                         <xsl:text>.</xsl:text>
 788                         <xsl:apply-templates select="*[position()=3]">
 789                         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 790                         </xsl:apply-templates>
 791                 </xsl:when>
 792                 <xsl:otherwise>
 793                         <xsl:apply-templates mode="inline" select="."/>
 794                 </xsl:otherwise>
 795        </xsl:choose>
 796       </xsl:when>
 797
 798     <!-- ARROW --> <!-- FUNCTION IND -->
 799         <xsl:when test="$name='arrow'">
 800                 <xsl:choose>
 801                         <xsl:when test="$charlength > $framewidth">
 802                         <xsl:text>arrow</xsl:text>
 803                         <xsl:text>(</xsl:text>
 804                         <xsl:apply-templates select="*[position()=2]">
 805                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 806                         </xsl:apply-templates>
 807                         <br/>
 808                         <xsl:call-template name="make_indent">
 809                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 810                         </xsl:call-template>
 811                 <!-- -> -->
 812                         <xsl:text> </xsl:text>
 813                         <xsl:call-template name="mksymbol">
 814                                 <xsl:with-param name="symbol" select="$arrow"/>
 815                                 <xsl:with-param name="color" select="'blue'"/>
 816                                 <xsl:with-param name="size" select="'+0'"/>
 817                         </xsl:call-template>
 818                         <xsl:apply-templates select="*[position()=3]">
 819                                 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 820                         </xsl:apply-templates>
 821                         <xsl:text>)</xsl:text>
 822                 </xsl:when>
 823                 <xsl:otherwise>
 824                         <xsl:apply-templates mode="inline" select="."/>
 825                 </xsl:otherwise>
 826         </xsl:choose>
 827 </xsl:when>
 828
 829      <!-- TYPE_OF -->
 830      <xsl:when test="$name='type_of'">
 831         <xsl:value-of select="*[2]"/>
 832          <xsl:text>:</xsl:text>
 833         <xsl:if test="count(*[3]/*) > 1">
 834                 <xsl:text>(</xsl:text>
 835         </xsl:if>
 836         <xsl:apply-templates select="*[3]"/>
 837         <xsl:if test="count(*[3]/*) > 1">
 838                 <xsl:text>)</xsl:text>
 839         </xsl:if>
 840       </xsl:when>
 841
 842         <!-- AXIOM -->
 843         <xsl:when test="$name='Ax'">
 844                 <FONT color="blue">
 845                 <xsl:text>Ax</xsl:text>
 846                 </FONT>
 847         </xsl:when>
 848
 849         <!-- VOID -->
 850         <xsl:when test="$name='void'">
 851                 <FONT color="blue">
 852                 <xsl:text>Void</xsl:text>
 853                 </FONT>
 854         </xsl:when>
 855
 856         <!-- ATOM -->
 857         <xsl:when test="$name='atom'">
 858                 <FONT color="blue">
 859                 <xsl:text>Atom</xsl:text>
 860                 </FONT>
 861         </xsl:when>
 862
 863
 864
 865      <!-- FORALL -->
 866      <xsl:when test="$name='forall'">
 867        <xsl:choose>
 868        <xsl:when test="$charlength > $framewidth">
 869         <!-- &#x03a0; -->
 870          <xsl:call-template name="mksymbol">
 871           <xsl:with-param name="symbol" select="$forall"/>
 872           <xsl:with-param name="color" select="'blue'"/>
 873           <xsl:with-param name="size" select="'+2'"/>
 874          </xsl:call-template>
 875          <xsl:apply-templates select="m:bvar/m:ci">
 876          <xsl:with-param name="current_indent" select="$current_indent"/>
 877          </xsl:apply-templates>
 878          <xsl:text>:</xsl:text>
 879          <xsl:apply-templates select="m:bvar/m:type">
 880           <xsl:with-param name="current_indent"
 881            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 882          </xsl:apply-templates>
 883          <br/>
 884          <xsl:call-template name="make_indent">
 885           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 886          </xsl:call-template>
 887          <xsl:text>.</xsl:text>
 888          <xsl:apply-templates select="*[position()=3]">
 889           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 890          </xsl:apply-templates>
 891        </xsl:when>
 892        <xsl:otherwise>
 893         <xsl:apply-templates mode="inline" select="."/>
 894        </xsl:otherwise>
 895        </xsl:choose>
 896       </xsl:when>
 897
 898       <!-- PRODUCT -->
 899       <xsl:when test="$name='product'">
 900        <xsl:choose>
 901        <xsl:when test="$charlength > $framewidth">
 902          <xsl:call-template name="mksymbol">
 903           <xsl:with-param name="symbol" select="$product"/>
 904           <xsl:with-param name="color" select="'blue'"/>
 905           <xsl:with-param name="size" select="'+2'"/>
 906          </xsl:call-template>
 907          <xsl:apply-templates select="m:bvar/m:ci">
 908           <xsl:with-param name="current_indent" select="$current_indent"/>
 909          </xsl:apply-templates>
 910          <xsl:text>:</xsl:text>
 911          <xsl:apply-templates select="m:bvar/m:type">
 912           <xsl:with-param name="current_indent"
 913            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 914          </xsl:apply-templates><br/>
 915          <xsl:call-template name="make_indent">
 916           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 917          </xsl:call-template>
 918          <xsl:text>.</xsl:text>
 919          <xsl:apply-templates select="*[position()=3]">
 920           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 921          </xsl:apply-templates>
 922        </xsl:when>
 923        <xsl:otherwise>
 924         <xsl:apply-templates mode="inline" select="."/>
 925        </xsl:otherwise>
 926        </xsl:choose>
 927       </xsl:when>
 928
 929        <!-- PROD_IND -->
 930       <xsl:when test="$name='product_ind'">
 931        <xsl:choose>
 932        <xsl:when test="$charlength > $framewidth">
 933        <FONT color="blue">
 934                 <xsl:text>( </xsl:text>
 935         </FONT>
 936          <xsl:apply-templates select="m:type">
 937           <xsl:with-param name="current_indent"
 938            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 939          </xsl:apply-templates>
 940          <br/>
 941          <xsl:call-template name="make_indent">
 942           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 943          </xsl:call-template>
 944         <FONT color="blue" size="+1">
 945          <xsl:text> x </xsl:text>
 946          </FONT>
 947          <xsl:apply-templates select="*[position()=3]">
 948           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 949          </xsl:apply-templates>
 950          <FONT color="blue">
 951                 <xsl:text> )</xsl:text>
 952         </FONT>
 953        </xsl:when>
 954        <xsl:otherwise>
 955         <xsl:apply-templates mode="inline" select="."/>
 956        </xsl:otherwise>
 957        </xsl:choose>
 958       </xsl:when>
 959
 960       <!-- PAIR -->
 961         <xsl:when test="$name='pair'">
 962                 <xsl:choose>
 963                 <xsl:when test="$charlength > $framewidth">
 964                         <FONT color="blue" size="+1">
 965                         <xsl:text>&lt;</xsl:text>
 966                         </FONT>
 967                         <xsl:apply-templates select="*[position()=2]">
 968                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 969                         </xsl:apply-templates>
 970                         <xsl:text>, </xsl:text>
 971                         <br/>
 972                         <xsl:call-template name="make_indent">
 973                         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 974                         </xsl:call-template>
 975                         <xsl:apply-templates select="*[position()=3]">
 976                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 977                         </xsl:apply-templates>
 978                         <FONT color="blue" size="+1">
 979                         <xsl:text>&gt;</xsl:text>
 980                         </FONT>
 981                 </xsl:when>
 982                 <xsl:otherwise>
 983                         <xsl:apply-templates mode="inline" select="."/>
 984                 </xsl:otherwise>
 985                 </xsl:choose>
 986         </xsl:when>
 987
 988         <!-- UNION -->
 989                 <xsl:when test="$name='union'">
 990                 <xsl:choose>
 991                 <xsl:when test="$charlength > $framewidth">
 992                         <xsl:apply-templates select="*[position()=2]">
 993                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 994                         </xsl:apply-templates>
 995                         <br/>
 996                         <xsl:call-template name="make_indent">
 997                         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 998                         </xsl:call-template>
 999                         <FONT color="blue" size="+1">
1000                         <xsl:text>+</xsl:text>
1001                         </FONT>
1002                         <xsl:apply-templates select="*[position()=3]">
1003                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1004                         </xsl:apply-templates>
1005                 </xsl:when>
1006                 <xsl:otherwise>
1007                         <xsl:apply-templates mode="inline" select="."/>
1008                 </xsl:otherwise>
1009                 </xsl:choose>
1010         </xsl:when>
1011
1012      <!-- INL -->
1013         <xsl:when test="$name='inl'">
1014                 <xsl:choose>
1015                 <xsl:when test="$charlength > $framewidth">
1016                         <FONT color="blue">
1017                         <xsl:text>inl (</xsl:text>
1018                         </FONT>
1019                         <xsl:apply-templates select="*[position()=2]">
1020                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1021                         </xsl:apply-templates>
1022                         <FONT color="blue">
1023                         <xsl:text> )</xsl:text>
1024                         </FONT>
1025                 </xsl:when>
1026                 <xsl:otherwise>
1027                         <xsl:apply-templates mode="inline" select="."/>
1028                 </xsl:otherwise>
1029                 </xsl:choose>
1030         </xsl:when>
1031
1032         <!-- INR -->
1033         <xsl:when test="$name='inr'">
1034                 <xsl:choose>
1035                 <xsl:when test="$charlength > $framewidth">
1036                         <FONT color="blue" size="+1">
1037                         <xsl:text>inr (</xsl:text>
1038                         </FONT>
1039                         <xsl:apply-templates select="*[position()=2]">
1040                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1041                         </xsl:apply-templates>
1042                         <FONT color="blue" size="+1">
1043                         <xsl:text> )</xsl:text>
1044                         </FONT>
1045                 </xsl:when>
1046                 <xsl:otherwise>
1047                         <xsl:apply-templates mode="inline" select="."/>
1048                 </xsl:otherwise>
1049                 </xsl:choose>
1050         </xsl:when>
1051
1052         <!-- PROP -->
1053         <xsl:when test="$name='prop'">
1054                 <FONT color="blue">
1055                 <xsl:text>P</xsl:text>
1056                 </FONT>
1057                 <FONT color="blue" size="-2">
1058                 <xsl:apply-templates select="m:cn">
1059                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1060                 </xsl:apply-templates>
1061                 </FONT>
1062         </xsl:when>
1063
1064         <!-- UNIVERSE -->
1065         <xsl:when test="$name='universe'">
1066                 <FONT color="blue" size="+1">
1067                 <xsl:text>U</xsl:text>
1068                 </FONT>
1069                 <FONT color="blue" size="2">
1070                 <xsl:apply-templates select="m:cn"/>
1071                 </FONT>
1072         </xsl:when>
1073
1074         <!-- EQUAL -->
1075         <xsl:when test="$name='equal'">
1076                 <xsl:choose>
1077                         <xsl:when test="$charlength > $framewidth">
1078                         <xsl:apply-templates select="*[position()=3]">
1079                          <xsl:with-param name="current_indent" select="$current_indent"/>
1080                         </xsl:apply-templates>
1081                         <br/>
1082                         <xsl:call-template name="make_indent">
1083                          <xsl:with-param name="current_indent" select="$current_indent"/>
1084                         </xsl:call-template>
1085                         <FONT color="blue" size="+1">
1086                          <xsl:text>= </xsl:text>
1087                         </FONT>
1088                         <xsl:apply-templates select="*[position()=4]">
1089                          <xsl:with-param name="current_indent" select="$current_indent"/>
1090                         </xsl:apply-templates>
1091                         <br/>
1092                         <xsl:call-template name="make_indent">
1093                         <xsl:with-param name="current_indent" select="$current_indent"/>
1094                         </xsl:call-template>
1095                         <!-- member -->
1096                         <xsl:call-template name="mksymbol">
1097                         <xsl:with-param name="symbol" select="$member"/>
1098                         <xsl:with-param name="color" select="'blue'"/>
1099                         <xsl:with-param name="size" select="'+0'"/>
1100                         </xsl:call-template>
1101                         <xsl:apply-templates select="*[position()=2]">
1102                         <xsl:with-param name="current_indent" select="$current_indent"/>
1103                         </xsl:apply-templates>
1104                 </xsl:when>
1105                 <xsl:otherwise>
1106                         <xsl:apply-templates mode="inline" select="."/>
1107                 </xsl:otherwise>
1108        </xsl:choose>
1109       </xsl:when>
1110
1111         <!-- TOKEN -->
1112
1113         <xsl:when test="$name='token'">
1114                 <FONT color="blue">
1115                 <xsl:text>"</xsl:text>
1116                 </FONT>
1117                 <xsl:apply-templates select="m:ci"/>
1118                 <FONT color="blue">
1119                 <xsl:text>"</xsl:text>
1120                 </FONT>
1121         </xsl:when>
1122
1123         <!-- NIL -->
1124
1125         <xsl:when test="$name='nil'">
1126                 <FONT color="blue">
1127                 <xsl:text>[]</xsl:text>
1128                 </FONT>
1129         </xsl:when>
1130
1131         <!-- CONS -->
1132         <xsl:when test="$name='cons'">
1133                 <xsl:apply-templates select="*[2]">
1134                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1135                 </xsl:apply-templates>
1136                 <br/>
1137                 <xsl:call-template name="make_indent">
1138                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1139                 </xsl:call-template>
1140                 <FONT color="blue">
1141                 <xsl:text>::</xsl:text>
1142                 </FONT>
1143                 <xsl:apply-templates select="*[3]">
1144                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1145                 </xsl:apply-templates>
1146         </xsl:when>
1147
1148
1149         <!-- REC -->
1150
1151         <xsl:when test="$name='rec'">
1152                 <xsl:choose>
1153                 <xsl:when test="$charlength > $framewidth">
1154                 <FONT color="blue">
1155                 <xsl:text>rectype</xsl:text>
1156                 </FONT>
1157                 <xsl:apply-templates select="*[2]">
1158                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1159                 </xsl:apply-templates>
1160                 <br/>
1161                 <xsl:call-template name="make_indent">
1162                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1163                 </xsl:call-template>
1164                 <FONT color="blue">
1165                 <xsl:text>=</xsl:text>
1166                 </FONT>
1167                 <xsl:apply-templates select="*[3]">
1168                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1169                 </xsl:apply-templates>
1170                 </xsl:when>
1171                 <xsl:otherwise>
1172                         <xsl:apply-templates mode="inline" select="."/>
1173                 </xsl:otherwise>
1174                 </xsl:choose>
1175         </xsl:when>
1176
1177         <!-- SET -->
1178
1179         <xsl:when test="$name='t_set'">
1180         <xsl:choose>
1181                 <xsl:when test="$charlength > $framewidth">
1182                 <FONT color="blue">
1183                 <xsl:text>{</xsl:text>
1184                 </FONT>
1185                 <xsl:choose>
1186                 <xsl:when test="m:bvar/m:ci">
1187                         <xsl:apply-templates select="m:bvar/m:ci"/>
1188                         <FONT color="blue">
1189                                 <xsl:text>:</xsl:text>
1190                         </FONT>
1191                         <xsl:apply-templates select="m:bvar/m:type">
1192                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1193                         </xsl:apply-templates>
1194                         <br/>
1195                         <xsl:call-template name="make_indent">
1196                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1197                         </xsl:call-template>
1198                 </xsl:when>
1199                 <xsl:otherwise>
1200                         <xsl:apply-templates select="m:bvar/m:type">
1201                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1202                         </xsl:apply-templates>
1203                         <br/>
1204                         <xsl:call-template name="make_indent">
1205                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1206                         </xsl:call-template>
1207                 </xsl:otherwise>
1208                 </xsl:choose>
1209                 <FONT color="blue">
1210                         <xsl:text>|</xsl:text>
1211                 </FONT>
1212                 <xsl:apply-templates select="*[3]">
1213                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1214                 </xsl:apply-templates>
1215
1216                 <FONT color="blue">
1217                         <xsl:text>}</xsl:text>
1218                 </FONT>
1219
1220                 </xsl:when>
1221                 <xsl:otherwise>
1222                         <xsl:apply-templates mode="inline" select="."/>
1223                 </xsl:otherwise>
1224                 </xsl:choose>
1225         </xsl:when>
1226
1227         <!-- ISECT -->
1228
1229         <xsl:when test="$name='isect'">
1230                 <xsl:call-template name="mksymbol">
1231                 <xsl:with-param name="symbol" select="$intersection"/>
1232                 <xsl:with-param name="color" select="'blue'"/>
1233                 <xsl:with-param name="size" select="'+0'"/>
1234                 </xsl:call-template>
1235                 <xsl:apply-templates select="m:bvar/m:ci"/>
1236                 <FONT color="blue">
1237                 <xsl:text>:</xsl:text>
1238                 </FONT>
1239                 <xsl:apply-templates select="m:bvar/m:type">
1240                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1241                 </xsl:apply-templates>
1242                 <br/>
1243                 <xsl:call-template name="make_indent">
1244                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1245                 </xsl:call-template>
1246                 <FONT color="blue">
1247                 <xsl:text>.</xsl:text>
1248                 </FONT>
1249                 <xsl:apply-templates select="*[3]">
1250                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1251                 </xsl:apply-templates>
1252
1253         </xsl:when>
1254
1255         <!-- QUOTIENT -->
1256
1257         <xsl:when test="$name='quotient'">
1258                 <xsl:apply-templates select="m:bvar[1]"/>
1259                 <xsl:text>,</xsl:text>
1260                 <xsl:apply-templates select="m:bvar[2]"/>
1261                 <FONT color="blue">
1262                 <xsl:text>:</xsl:text>
1263                 </FONT>
1264                 <xsl:apply-templates select="*[2]">
1265                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1266                 </xsl:apply-templates>
1267                 <br/>
1268                 <xsl:call-template name="make_indent">
1269                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1270                 </xsl:call-template>
1271                 <FONT color="blue">
1272                 <xsl:text>//</xsl:text>
1273                 </FONT>
1274                 <xsl:apply-templates select="*[5]">
1275                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1276                 </xsl:apply-templates>
1277
1278         </xsl:when>
1279
1280         <!-- IF_THEN_ELSE -->
1281         <xsl:when test="$name='if_then_else'">
1282                 <xsl:choose>
1283                 <xsl:when test="m:where = 'atom_eq'">
1284                         <FONT color="blue">
1285                         <xsl:text>atom_eq (</xsl:text>
1286                         </FONT>
1287                 </xsl:when>
1288                 <xsl:when test="m:where = 'int_eq'">
1289                         <FONT color="blue">
1290                         <xsl:text>int_eq (</xsl:text>
1291                         </FONT>
1292                 </xsl:when>
1293                 <xsl:when test="m:where = 'less'">
1294                         <FONT color="blue">
1295                         <xsl:text>less (</xsl:text>
1296                         </FONT>
1297                 </xsl:when>
1298                 </xsl:choose>
1299                 <xsl:apply-templates select="*[3]"/>
1300                 <xsl:text>; </xsl:text>
1301                 <xsl:apply-templates select="*[4]"/>
1302                 <xsl:text>; </xsl:text>
1303                 <xsl:apply-templates select="*[5]"/>
1304                 <xsl:text>; </xsl:text>
1305                 <xsl:apply-templates select="*[6]"/>
1306                 <FONT color="blue">
1307                 <xsl:text>)</xsl:text>
1308                 </FONT>
1309         </xsl:when>
1310
1311
1312         <!-- SO_LAMBDA -->
1313         <xsl:when test="$name='so_lambda'">
1314         <xsl:choose>
1315                 <xsl:when test="$charlength > $framewidth">
1316                         <xsl:call-template name="mksymbol">
1317                                 <xsl:with-param name="symbol" select="$lambda"/>
1318                                 <xsl:with-param name="color" select="'red'"/>
1319                                 <xsl:with-param name="size" select="'+2'"/>
1320                         </xsl:call-template>
1321                         <xsl:apply-templates select="m:apply[1]/*[2]"/>
1322                         <br/>
1323                         <xsl:call-template name="make_indent">
1324                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1325                         </xsl:call-template>
1326                         <xsl:text>.</xsl:text>
1327                         <xsl:apply-templates select="*[3]">
1328                          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1329                         </xsl:apply-templates>
1330                 </xsl:when>
1331                 <xsl:otherwise>
1332                         <xsl:apply-templates mode="inline" select="."/>
1333                 </xsl:otherwise>
1334      </xsl:choose>
1335      </xsl:when>
1336
1337
1338         <!-- SO_APPLY -->
1339
1340         <xsl:when test="$name='so_apply'">
1341         <xsl:choose>
1342         <xsl:when test="$charlength  > $framewidth">
1343                 <xsl:text>(</xsl:text>
1344                 <xsl:apply-templates select="*[position()=2]">
1345                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1346                 </xsl:apply-templates>
1347                 <xsl:for-each select="*[position()>2]">
1348                         <br/>
1349                         <xsl:call-template name="make_indent">
1350                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1351                         </xsl:call-template>
1352                         <xsl:apply-templates select=".">
1353                                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1354                         </xsl:apply-templates>
1355                 </xsl:for-each>
1356                 <xsl:text>)</xsl:text>
1357        </xsl:when>
1358        <xsl:otherwise>
1359                 <xsl:apply-templates mode="inline" select="."/>
1360        </xsl:otherwise>
1361        </xsl:choose>
1362       </xsl:when>
1363
1364       <!-- APP -->
1365       <xsl:when test="$name='app'">
1366         <xsl:choose>
1367         <xsl:when test="$charlength  > $framewidth">
1368          <!-- NuPRL rendering -->
1369          <xsl:apply-templates select="*[position()=2]">
1370           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1371          </xsl:apply-templates>
1372          <br/>
1373          <xsl:call-template name="make_indent">
1374           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1375          </xsl:call-template>
1376          <xsl:if test="count(*) &gt; 2">
1377           <xsl:text>(</xsl:text>
1378           <xsl:for-each select="*[position() &gt; 2]">
1379            <br/>
1380            <xsl:call-template name="make_indent">
1381             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1382            </xsl:call-template>
1383            <xsl:apply-templates select="." mode="inline"/>
1384            <xsl:if test="not(position() = last())">
1385             <xsl:text>,</xsl:text>
1386            </xsl:if>
1387           </xsl:for-each>
1388           <xsl:text>)</xsl:text>
1389          </xsl:if>
1390                 <!-- CIC rendering
1391                 <xsl:text>(</xsl:text>
1392                 <xsl:apply-templates select="*[position()=2]">
1393                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1394                 </xsl:apply-templates>
1395                 <xsl:for-each select="*[position()>2]">
1396                         <br/>
1397                         <xsl:call-template name="make_indent">
1398                         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1399                         </xsl:call-template>
1400                         <xsl:apply-templates select=".">
1401                         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1402                         </xsl:apply-templates>
1403                 </xsl:for-each>
1404                 <xsl:text>)</xsl:text>
1405                 -->
1406        </xsl:when>
1407        <xsl:otherwise>
1408                 <xsl:apply-templates mode="inline" select="."/>
1409        </xsl:otherwise>
1410        </xsl:choose>
1411       </xsl:when>
1412
1413       <xsl:when test="$name='cast'">
1414        <xsl:choose>
1415         <xsl:when test="$showcast = 1">
1416          <xsl:choose>
1417           <xsl:when test="$charlength > $framewidth">
1418            <xsl:text>(</xsl:text>
1419            <xsl:apply-templates select="*[position()=2]">
1420             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1421            </xsl:apply-templates><br/>
1422            <xsl:call-template name="make_indent">
1423             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1424            </xsl:call-template>
1425            <xsl:text>:</xsl:text>
1426            <xsl:apply-templates select="*[position()=3]">
1427             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1428            </xsl:apply-templates>
1429            <xsl:text>)</xsl:text>
1430           </xsl:when>
1431           <xsl:otherwise>
1432            <xsl:apply-templates mode="inline" select="."/>
1433           </xsl:otherwise>
1434          </xsl:choose>
1435         </xsl:when>
1436         <xsl:otherwise>
1437          <xsl:apply-templates select="*[position()=2]">
1438           <xsl:with-param name="current_indent" select="$current_indent"/>
1439          </xsl:apply-templates>
1440         </xsl:otherwise>
1441        </xsl:choose>
1442       </xsl:when>
1443       <xsl:when test="$name='Prop'">
1444        <xsl:text>Prop</xsl:text>
1445       </xsl:when>
1446       <xsl:when test="$name='Set'">
1447        <xsl:text>Set</xsl:text>
1448       </xsl:when>
1449       <xsl:when test="$name='Type'">
1450        <xsl:text>Type</xsl:text>
1451       </xsl:when>
1452       <xsl:when test="$name='mutcase'">
1453        <xsl:choose>
1454        <xsl:when test="$charlength > $framewidth">
1455          <xsl:text>&lt;</xsl:text>
1456          <xsl:apply-templates select="*[position()=2]">
1457           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1458          </xsl:apply-templates>
1459          <xsl:text>&gt; </xsl:text>
1460          <br/>
1461          <xsl:call-template name="make_indent">
1462           <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
1463          <xsl:text>CASE </xsl:text>
1464          <xsl:apply-templates select="*[position()=3]">
1465           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1466          </xsl:apply-templates>
1467          <xsl:text> OF </xsl:text>
1468          <xsl:for-each select="m:piecewise/m:piece">
1469     <!--   <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
1470          <br/>
1471          <xsl:call-template name="make_indent">
1472           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1473          </xsl:call-template>
1474             <xsl:choose>
1475             <xsl:when test="position() = 1">
1476              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1477             </xsl:when>
1478             <xsl:otherwise>
1479              <xsl:text>| </xsl:text>
1480             </xsl:otherwise>
1481             </xsl:choose>
1482           <xsl:apply-templates select="./*[2]"/>
1483             <xsl:call-template name="mksymbol">
1484              <xsl:with-param name="symbol" select="$RightArrow"/>
1485              <xsl:with-param name="color" select="'green'"/>
1486              <xsl:with-param name="size" select="'+0'"/>
1487             </xsl:call-template>
1488             <xsl:variable name="body_size">
1489   <xsl:apply-templates
1490               select="./*[1]/*[1]" mode="charcount"/>
1491             </xsl:variable>
1492             <xsl:choose>
1493              <xsl:when test="$body_size > $framewidth">
1494               <br/>
1495               <xsl:call-template name="make_indent">
1496                <xsl:with-param name="current_indent"
1497                     select="$current_indent + 8"/>
1498               </xsl:call-template>
1499 <xsl:apply-templates
1500                    select="./*[1]">
1501               <xsl:with-param name="current_indent"
1502                    select="$current_indent + 8"/>
1503              </xsl:apply-templates>
1504             </xsl:when>
1505             <xsl:otherwise>
1506      <xsl:apply-templates select="./*[1]"
1507                    mode="inline" />
1508             </xsl:otherwise>
1509            </xsl:choose>
1510          </xsl:for-each>
1511        </xsl:when>
1512        <xsl:otherwise>
1513         <xsl:apply-templates mode="inline" select="."/>
1514        </xsl:otherwise>
1515        </xsl:choose>
1516       </xsl:when>
1517       <!-- FIX -->
1518       <xsl:when test="$name='fix'">
1519        <xsl:choose>
1520        <xsl:when test="$charlength  > $framewidth">
1521             <xsl:text>FIX</xsl:text>
1522             <xsl:value-of select="m:ci"/>
1523             <xsl:text>{</xsl:text>
1524             <xsl:for-each select="m:bvar">
1525               <br/>
1526               <xsl:call-template name="make_indent">
1527                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1528               </xsl:call-template>
1529               <xsl:value-of select="m:ci"/>
1530               <xsl:text>:</xsl:text>
1531               <xsl:apply-templates select="m:type">
1532                <xsl:with-param name="current_indent"
1533                     select="$current_indent + 5 + string-length(m:ci)"/>
1534                </xsl:apply-templates>
1535               <br/>
1536               <xsl:call-template name="make_indent">
1537                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1538               </xsl:call-template>
1539               <xsl:text>:=</xsl:text>
1540               <xsl:apply-templates select="following-sibling::*[position() = 1]">
1541                <xsl:with-param name="current_indent" select="$current_indent +2"/>
1542               </xsl:apply-templates>
1543             </xsl:for-each>
1544              <br/>
1545               <xsl:call-template name="make_indent">
1546                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1547               </xsl:call-template>
1548            <xsl:text>}</xsl:text>
1549        </xsl:when>
1550        <xsl:otherwise>
1551         <xsl:apply-templates mode="inline" select="."/>
1552        </xsl:otherwise>
1553        </xsl:choose>
1554       </xsl:when>
1555       <!-- COFIX -->
1556       <xsl:when test="$name='cofix'">
1557        <xsl:choose>
1558        <xsl:when test="($charlength + 10) > $framewidth">
1559             <xsl:text>COFIX</xsl:text>
1560             <xsl:value-of select="m:ci"/>
1561             <xsl:text>{</xsl:text>
1562             <br/>
1563             <xsl:call-template name="make_indent">
1564              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1565             </xsl:call-template>
1566             <xsl:for-each select="m:bvar">
1567                 <xsl:value-of select="m:ci"/>
1568                 <xsl:text>:</xsl:text>
1569                 <xsl:apply-templates select="m:type">
1570                  <xsl:with-param name="current_indent"
1571                     select="$current_indent + 5 + string-length(m:ci)"/>
1572                 </xsl:apply-templates>
1573                 <br/>
1574                 <xsl:call-template name="make_indent">
1575                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1576                 </xsl:call-template>
1577                 <xsl:text>:=</xsl:text>
1578                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1579                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1580                 </xsl:apply-templates>
1581
1582             </xsl:for-each>
1583             <br/>
1584               <xsl:call-template name="make_indent">
1585                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1586               </xsl:call-template>
1587             <xsl:text>}</xsl:text>
1588        </xsl:when>
1589        <xsl:otherwise>
1590         <xsl:apply-templates mode="inline" select="m:type"/>
1591        </xsl:otherwise>
1592        </xsl:choose>
1593       </xsl:when>
1594       <xsl:when test="$name='let_in'">
1595        <xsl:text>let&#x00a0;</xsl:text>
1596        <xsl:apply-templates select="m:bvar/m:ci"/>
1597        <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
1598        <xsl:apply-templates select="*[3]">
1599         <xsl:with-param name="current_indent" select="$current_indent+14"/>
1600        </xsl:apply-templates>
1601        <br/>
1602        <xsl:call-template name="make_indent">
1603         <xsl:with-param name="current_indent" select="$current_indent"/>
1604        </xsl:call-template>
1605        <xsl:text>in&#x00a0;</xsl:text>
1606        <xsl:apply-templates select="*[4]">
1607         <xsl:with-param name="current_indent" select="$current_indent+5"/>
1608        </xsl:apply-templates>
1609       </xsl:when>
1610
1611       <!-- ***************************************** -->
1612       <!-- *********** PROOF ELEMENTS ************** -->
1613       <!-- ***************************************** -->
1614       <!-- PROOF -->
1615       <xsl:when test="$name='proof'">
1616        <xsl:variable name="nonce" select="generate-id()"/>
1617        <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1618        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1619        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1620        <span ID="{$freshid1}">
1621         <xsl:apply-templates select="*[position()=2]">
1622          <xsl:with-param name="current_indent" select="$current_indent"/>
1623         </xsl:apply-templates>
1624         &#x00a0;
1625        </span>
1626        <xsl:choose>
1627         <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
1628                         (preceding-sibling::*[1]/text()='rw_step') or
1629                         (name(..)='m:lambda')">
1630          <br/>
1631          <xsl:call-template name="make_indent">
1632           <xsl:with-param name="current_indent" select="$current_indent"/>
1633          </xsl:call-template>
1634          <FONT color="red">we proved&#x00a0;</FONT>
1635         </xsl:when>
1636         <xsl:otherwise>
1637          <script>
1638           if(document.getElementById) {
1639            document.write('\
1640             <span ID="{$freshid2}">\
1641              <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));return (0==1);">Proof of</a>\
1642             </span>\
1643             <span ID="{$freshid3}">\
1644              <br/>\
1645              <xsl:call-template name="make_indent">
1646               <xsl:with-param name="current_indent" select="$current_indent"/>
1647              </xsl:call-template>\
1648              <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
1649             </span>\
1650            ');
1651            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1652            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1653            document.write('&#x00a0;');
1654           } else {
1655            document.write('\
1656             <br/>\
1657             <xsl:call-template name="make_indent">
1658              <xsl:with-param name="current_indent" select="$current_indent"/>
1659             </xsl:call-template>\
1660             <FONT color="red">we proved&#x00a0;</FONT>\
1661            ');
1662           }
1663          </script>
1664         </xsl:otherwise>
1665        </xsl:choose>
1666        <xsl:apply-templates select="*[position()=3]">
1667         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1668        </xsl:apply-templates>
1669       </xsl:when>
1670       <!-- side_proof -->
1671       <xsl:when test="$name='side_proof'">
1672        <xsl:variable name="nonce" select="generate-id()"/>
1673        <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1674        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1675        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1676        <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
1677        <span ID="{$freshid1}">
1678         <xsl:apply-templates select="*[position()=2]">
1679          <xsl:with-param name="current_indent" select="$current_indent"/>
1680         </xsl:apply-templates>
1681         &#x00a0;
1682        </span>
1683          <script>
1684           if(document.getElementById) {
1685            document.write('\
1686             <span ID="{$freshid2}">\
1687              <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
1688             </span>\
1689             <span ID="{$freshid3}">\
1690              <br/>\
1691              <xsl:call-template name="make_indent">
1692               <xsl:with-param name="current_indent" select="$current_indent"/>
1693              </xsl:call-template>\
1694              <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
1695             </span>\
1696            ');
1697            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1698            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1699            document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
1700            document.write('&#x00a0;');
1701           } else {
1702            document.write('\
1703             <br/>\
1704             <xsl:call-template name="make_indent">
1705              <xsl:with-param name="current_indent" select="$current_indent"/>
1706             </xsl:call-template>\
1707             <FONT color="red">we proved&#x00a0;</FONT>\
1708            ');
1709           }
1710          </script>
1711        <span ID="{$freshid4}">
1712         <xsl:apply-templates select="*[position()=3]">
1713          <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1714         </xsl:apply-templates>
1715        </span>
1716       </xsl:when>
1717       <!-- eq_chain -->
1718       <xsl:when test="$name='eq_chain'">
1719        <FONT color="red">We have the following equality chain:</FONT>
1720        <xsl:for-each select="*[position() mod 2 = 0]">
1721         <xsl:variable name="pos" select="position()"/>
1722         <br/>
1723         <xsl:call-template name="make_indent">
1724          <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1725         </xsl:call-template>
1726         <xsl:choose>
1727          <xsl:when test="$pos=1">
1728           <xsl:apply-templates select=".">
1729            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1730           </xsl:apply-templates>
1731           <xsl:text>&#x00a0;=</xsl:text>
1732          </xsl:when>
1733          <xsl:otherwise>
1734           <xsl:text>=&#x00a0;</xsl:text>
1735           <xsl:apply-templates select=".">
1736            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1737           </xsl:apply-templates>
1738          </xsl:otherwise>
1739         </xsl:choose>
1740         <xsl:if test="$pos != last()">
1741          <br/>
1742          <xsl:call-template name="make_indent">
1743           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1744          </xsl:call-template>
1745          <xsl:apply-templates select="../*[position()=2*$pos +1]">
1746           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1747          </xsl:apply-templates>
1748         </xsl:if>
1749        </xsl:for-each>
1750       </xsl:when>
1751        <!-- diseq_chain -->
1752       <xsl:when test="$name='diseq_chain'">
1753        <FONT color="red">We have the following chain of disequalities:</FONT>
1754        <xsl:for-each select="*[position() mod 3 = 2]">
1755         <xsl:variable name="pos" select="position()"/>
1756         <br/>
1757         <xsl:call-template name="make_indent">
1758          <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1759         </xsl:call-template>
1760         <xsl:choose>
1761          <xsl:when test="$pos=1">
1762           <xsl:apply-templates select=".">
1763            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1764           </xsl:apply-templates>
1765           <xsl:text>&#x00a0;</xsl:text>
1766           <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
1767          </xsl:when>
1768          <xsl:otherwise>
1769           <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
1770           <xsl:text>&#x00a0;</xsl:text>
1771           <xsl:apply-templates select=".">
1772            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1773           </xsl:apply-templates>
1774          </xsl:otherwise>
1775         </xsl:choose>
1776         <xsl:if test="$pos != last()">
1777          <br/>
1778          <xsl:call-template name="make_indent">
1779           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1780          </xsl:call-template>
1781          <xsl:apply-templates select="../*[position()=3*$pos +1]">
1782           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1783          </xsl:apply-templates>
1784         </xsl:if>
1785        </xsl:for-each>
1786       </xsl:when>
1787       <!-- letin1 -->
1788       <xsl:when test="$name='letin1'">
1789        <xsl:apply-templates select="*[position()=2]">
1790         <xsl:with-param name="current_indent" select="$current_indent"/>
1791        </xsl:apply-templates>
1792        <br/>
1793        <xsl:call-template name="make_indent">
1794         <xsl:with-param name="current_indent" select="$current_indent"/>
1795        </xsl:call-template>
1796        <xsl:apply-templates select="*[position()=3]">
1797         <xsl:with-param name="current_indent" select="$current_indent"/>
1798        </xsl:apply-templates>
1799       </xsl:when>
1800       <!-- letin -->
1801       <xsl:when test="$name='letin'">
1802        <xsl:for-each select="*[position()>1 and last()>position()]">
1803         <xsl:apply-templates select=".">
1804          <xsl:with-param name="current_indent" select="$current_indent"/>
1805         </xsl:apply-templates>
1806         <br/>
1807         <xsl:call-template name="make_indent">
1808          <xsl:with-param name="current_indent" select="$current_indent"/>
1809         </xsl:call-template>
1810        </xsl:for-each>
1811        <xsl:apply-templates select="*[position()=last()]">
1812         <xsl:with-param name="current_indent" select="$current_indent"/>
1813        </xsl:apply-templates>
1814       </xsl:when>
1815       <!-- Let -->
1816       <xsl:when test="$name='let'">
1817        (
1818        <xsl:apply-templates select="m:ci"/>
1819        )
1820        <xsl:apply-templates select="*[3]">
1821         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1822        </xsl:apply-templates>
1823       </xsl:when>
1824       <!-- rw_step -->
1825       <xsl:when test="$name='rw_step'">
1826        <xsl:choose>
1827         <xsl:when test="name(*[2])='m:apply'">
1828          <xsl:apply-templates select="*[2]">
1829           <xsl:with-param name="current_indent" select="$current_indent"/>
1830          </xsl:apply-templates>
1831         </xsl:when>
1832         <xsl:otherwise>
1833          <FONT color="red">Consider&#x00a0;</FONT>
1834          <xsl:apply-templates select="*[2]"/>
1835         </xsl:otherwise>
1836        </xsl:choose>
1837        <xsl:variable name="charlength_first">
1838         <xsl:apply-templates select="*[3]" mode="root_charcount"/>
1839        </xsl:variable>
1840        <xsl:variable name="charlength_second">
1841         <xsl:apply-templates select="*[4]" mode="root_charcount"/>
1842        </xsl:variable>
1843        <xsl:variable name="charlength_side_proof">
1844         <xsl:apply-templates select="*[5]" mode="root_charcount"/>
1845        </xsl:variable>
1846        <xsl:variable name="split1"
1847          select="($charlength_first + $charlength_second) > $framewidth"/>
1848        <xsl:variable name="split2"
1849          select="($charlength_second + $charlength_side_proof) > $framewidth"/>
1850      <!-- <xsl:value-of select="$current_indent"/> -->
1851      <!-- <xsl:value-of select="string($charlength_second)"/>  -->
1852      <!-- <xsl:value-of select="$charlength_side_proof"/>  -->
1853      <!-- <xsl:value-of select="$split2"/>  -->
1854        <br/>
1855        <xsl:call-template name="make_indent">
1856         <xsl:with-param name="current_indent" select="$current_indent"/>
1857        </xsl:call-template>
1858        <FONT color="red">Rewrite&#x00a0;</FONT>
1859        <xsl:apply-templates mode="inline" select="*[3]"/>
1860        <xsl:text>&#x00a0;</xsl:text>
1861        <xsl:if test="$split1">
1862        <br/>
1863        <xsl:call-template name="make_indent">
1864         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1865        </xsl:call-template>
1866        </xsl:if>
1867        <FONT color="red">with&#x00a0;</FONT>
1868        <xsl:apply-templates mode="inline" select="*[4]"/>
1869        <xsl:text>&#x00a0;</xsl:text>
1870        <xsl:if test="$split2">
1871        <br/>
1872        <xsl:call-template name="make_indent">
1873         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1874        </xsl:call-template>
1875        </xsl:if>
1876        <FONT color="red">by&#x00a0;</FONT>
1877        <xsl:apply-templates select="*[5]">
1878         <xsl:with-param name="current_indent" select="$current_indent+7"/>
1879        </xsl:apply-templates>
1880       </xsl:when>
1881       <!-- rewrite and apply -->
1882       <xsl:when test="$name='rewrite_and_apply'">
1883        <xsl:apply-templates select="*[2]">
1884         <xsl:with-param name="current_indent" select="$current_indent"/>
1885        </xsl:apply-templates>
1886        <br/>
1887        <xsl:call-template name="make_indent">
1888         <xsl:with-param name="current_indent" select="$current_indent"/>
1889        </xsl:call-template>
1890        <FONT color="red">Then apply it to&#x00a0;</FONT>
1891        <xsl:apply-templates select="*[position()>2]"/>
1892       </xsl:when>
1893       <!-- by_induction -->
1894       <xsl:when test="$name='by_induction'">
1895        <FONT color="red">We prove&#x00a0;</FONT>
1896        <xsl:apply-templates select="../*[3]">
1897         <xsl:with-param name="current_indent" select="$current_indent+18"/>
1898        </xsl:apply-templates>
1899        <br/>
1900        <xsl:call-template name="make_indent">
1901         <xsl:with-param name="current_indent" select="$current_indent"/>
1902        </xsl:call-template>
1903        <FONT color="red">by induction on&#x00a0;</FONT>
1904        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
1905         <xsl:with-param name="current_indent" select="$current_indent+30"/>
1906        </xsl:apply-templates>
1907        <!--
1908        <br/>
1909        <xsl:call-template name="make_indent">
1910         <xsl:with-param name="current_indent" select="$current_indent"/>
1911        </xsl:call-template>
1912        <xsl:text>The induction property is</xsl:text>
1913        <br/>
1914        <xsl:call-template name="make_indent">
1915         <xsl:with-param name="current_indent" select="$current_indent"/>
1916        </xsl:call-template>
1917        <xsl:apply-templates select="*[3]">
1918         <xsl:with-param name="current_indent" select="$current_indent"/>
1919        </xsl:apply-templates>
1920        -->
1921        <xsl:apply-templates
1922             select="*[position()>3 and not(position()=last())]">
1923         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1924        </xsl:apply-templates>
1925        <!-- <br/>
1926        <xsl:call-template name="make_indent">
1927         <xsl:with-param name="current_indent" select="$current_indent"/>
1928        </xsl:call-template>
1929        <xsl:text>End induction</xsl:text> -->
1930       </xsl:when>
1931       <!-- inductive_case -->
1932       <xsl:when test="$name='inductive_case'">
1933        <br/>
1934        <xsl:call-template name="make_indent">
1935         <xsl:with-param name="current_indent" select="$current_indent"/>
1936        </xsl:call-template>
1937        <FONT color="red">Case&#x00a0;</FONT>
1938        <xsl:apply-templates select="*[2]">
1939         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1940        </xsl:apply-templates>
1941        <xsl:if test="*[3]/*[position()>1]">
1942         <br/>
1943         <xsl:call-template name="make_indent">
1944          <xsl:with-param name="current_indent" select="$current_indent+4"/>
1945         </xsl:call-template>
1946         <FONT color="red">By induction hypothesis, we have:</FONT>
1947         <xsl:for-each select="*[3]/*[position()>1]">
1948          <br/>
1949          <xsl:call-template name="make_indent">
1950           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1951          </xsl:call-template>
1952          <xsl:text>(</xsl:text>
1953          <xsl:apply-templates select="m:ci"/>
1954          <xsl:text>)&#x00a0;</xsl:text>
1955          <xsl:apply-templates select="m:type">
1956           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1957          </xsl:apply-templates>
1958         </xsl:for-each>
1959        </xsl:if>
1960        <br/>
1961         <xsl:call-template name="make_indent">
1962          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1963         </xsl:call-template>
1964        <xsl:apply-templates select="*[4]">
1965         <xsl:with-param name="current_indent" select="$current_indent +4"/>
1966        </xsl:apply-templates>
1967        <!-- <br/>
1968        <xsl:call-template name="make_indent">
1969         <xsl:with-param name="current_indent" select="$current_indent"/>
1970        </xsl:call-template>
1971        <xsl:text>End Case</xsl:text> -->
1972       </xsl:when>
1973       <!-- case_lhs  -->
1974       <xsl:when test="$name='case_lhs'">
1975        <xsl:choose>
1976         <xsl:when test="count(*)=2">
1977          <xsl:apply-templates mode="inline" select="*[2]"/>
1978         </xsl:when>
1979         <xsl:otherwise>
1980          <xsl:text>(</xsl:text>
1981          <xsl:apply-templates mode="inline" select="*[2]"/>
1982          <xsl:for-each select="m:bvar">
1983           <xsl:text>&#x00a0;</xsl:text>
1984           <xsl:apply-templates mode="inline" select="*[1]"/>
1985           <xsl:text>:</xsl:text>
1986           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1987          </xsl:for-each>
1988          <xsl:text>)</xsl:text>
1989         </xsl:otherwise>
1990        </xsl:choose>
1991       </xsl:when>
1992       <!-- false_ind -->
1993       <xsl:when test="$name='false_ind'">
1994        <xsl:apply-templates select="*[3]">
1995         <xsl:with-param name="current_indent" select="$current_indent"/>
1996        </xsl:apply-templates>
1997        <br/>
1998        <xsl:call-template name="make_indent">
1999         <xsl:with-param name="current_indent" select="$current_indent"/>
2000        </xsl:call-template>
2001        <FONT color="red">Contradiction.</FONT>
2002       </xsl:when>
2003       <!-- and_ind -->
2004       <xsl:when test="$name='and_ind'">
2005        <xsl:choose>
2006         <xsl:when test="name(*[2])='m:apply'">
2007          <xsl:apply-templates select="*[2]">
2008           <xsl:with-param name="current_indent" select="$current_indent"/>
2009          </xsl:apply-templates>
2010         </xsl:when>
2011         <xsl:otherwise>
2012          <FONT color="red">Consider&#x00a0;</FONT>
2013          <xsl:apply-templates select="*[2]"/>
2014         </xsl:otherwise>
2015        </xsl:choose>
2016        <br/>
2017        <xsl:call-template name="make_indent">
2018         <xsl:with-param name="current_indent" select="$current_indent"/>
2019        </xsl:call-template>
2020        <FONT color="red">In particular, we have</FONT>
2021        <br/>
2022        <xsl:call-template name="make_indent">
2023         <xsl:with-param name="current_indent" select="$current_indent"/>
2024        </xsl:call-template>
2025        (
2026        <xsl:apply-templates select="*[3]"/>
2027        )&#x00a0;
2028        <xsl:apply-templates select="*[4]">
2029         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2030        </xsl:apply-templates>
2031        <br/>
2032        <xsl:call-template name="make_indent">
2033         <xsl:with-param name="current_indent" select="$current_indent"/>
2034        </xsl:call-template>
2035        (
2036        <xsl:apply-templates select="*[5]"/>
2037        )&#x00a0;
2038        <xsl:apply-templates select="*[6]">
2039         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2040        </xsl:apply-templates>
2041        <br/>
2042        <xsl:call-template name="make_indent">
2043         <xsl:with-param name="current_indent" select="$current_indent"/>
2044        </xsl:call-template>
2045        <xsl:apply-templates select="*[7]">
2046         <xsl:with-param name="current_indent" select="$current_indent"/>
2047        </xsl:apply-templates>
2048       </xsl:when>
2049       <!-- full_or_ind -->
2050       <xsl:when test="$name='full_or_ind'">
2051        <xsl:choose>
2052         <xsl:when test="name(*[2])='m:apply'">
2053          <xsl:apply-templates select="*[2]">
2054           <xsl:with-param name="current_indent" select="$current_indent"/>
2055          </xsl:apply-templates>
2056         </xsl:when>
2057         <xsl:otherwise>
2058          <FONT color="red">Consider&#x00a0;</FONT>
2059          <xsl:apply-templates select="*[2]"/>
2060         </xsl:otherwise>
2061        </xsl:choose>
2062        <br/>
2063        <xsl:call-template name="make_indent">
2064         <xsl:with-param name="current_indent" select="$current_indent"/>
2065        </xsl:call-template>
2066        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
2067        <xsl:apply-templates select="*[3]"/>
2068        <br/>
2069        <xsl:call-template name="make_indent">
2070         <xsl:with-param name="current_indent" select="$current_indent+4"/>
2071        </xsl:call-template>
2072        <FONT color="red">Left: suppose&#x00a0;</FONT>
2073        <xsl:text>(</xsl:text>
2074        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
2075        <xsl:text>)&#x00a0;</xsl:text>
2076        <xsl:apply-templates
2077             select="*[4]/m:bvar/m:type/*[1]"/>
2078        <br/>
2079        <xsl:call-template name="make_indent">
2080         <xsl:with-param name="current_indent" select="$current_indent+15"/>
2081        </xsl:call-template>
2082        <xsl:apply-templates
2083             select="*[4]/*[3]">
2084         <xsl:with-param name="current_indent" select="$current_indent+15"/>
2085        </xsl:apply-templates>
2086        <br/>
2087        <xsl:call-template name="make_indent">
2088         <xsl:with-param name="current_indent" select="$current_indent+4"/>
2089        </xsl:call-template>
2090        <FONT color="red">Right: suppose&#x00a0;</FONT>
2091        <xsl:text>(</xsl:text>
2092        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
2093        <xsl:text>)&#x00a0;</xsl:text>
2094        <xsl:apply-templates
2095             select="*[5]/m:bvar/m:type/*[1]"/>
2096        <br/>
2097        <xsl:call-template name="make_indent">
2098         <xsl:with-param name="current_indent" select="$current_indent+16"/>
2099        </xsl:call-template>
2100        <xsl:apply-templates
2101             select="*[5]/*[3]">
2102         <xsl:with-param name="current_indent" select="$current_indent+16"/>
2103        </xsl:apply-templates>
2104       </xsl:when>
2105       <!-- or_ind -->
2106       <xsl:when test="$name='or_ind'">
2107        <xsl:choose>
2108         <xsl:when test="name(*[2])='m:apply'">
2109          <xsl:apply-templates select="*[2]">
2110           <xsl:with-param name="current_indent" select="$current_indent"/>
2111          </xsl:apply-templates>
2112         </xsl:when>
2113         <xsl:otherwise>
2114          <FONT color="red">Consider&#x00a0;</FONT>
2115          <xsl:apply-templates select="*[2]"/>
2116         </xsl:otherwise>
2117        </xsl:choose>
2118        <br/>
2119        <xsl:call-template name="make_indent">
2120         <xsl:with-param name="current_indent" select="$current_indent"/>
2121        </xsl:call-template>
2122        <FONT color="red">We prove&#x00a0;</FONT>
2123        <xsl:apply-templates select="*[3]"/>
2124        <FONT color="red">&#x00a0;by cases:</FONT>
2125        <br/>
2126        <xsl:call-template name="make_indent">
2127         <xsl:with-param name="current_indent" select="$current_indent"/>
2128        </xsl:call-template>
2129        Left:&#x00a0;
2130        <xsl:apply-templates select="*[4]">
2131         <xsl:with-param name="current_indent" select="$current_indent"/>
2132        </xsl:apply-templates>
2133        <br/>
2134        <xsl:call-template name="make_indent">
2135         <xsl:with-param name="current_indent" select="$current_indent"/>
2136        </xsl:call-template>
2137        Right:&#x00a0;
2138        <xsl:apply-templates select="*[5]">
2139         <xsl:with-param name="current_indent" select="$current_indent"/>
2140        </xsl:apply-templates>
2141       </xsl:when>
2142       <!-- Ex_ind -->
2143       <xsl:when test="$name='ex_ind'">
2144        <xsl:choose>
2145         <xsl:when test="name(*[2])='m:apply'">
2146          <xsl:apply-templates select="*[2]">
2147           <xsl:with-param name="current_indent" select="$current_indent"/>
2148          </xsl:apply-templates>
2149         </xsl:when>
2150         <xsl:otherwise>
2151          <FONT color="red">Consider&#x00a0;</FONT>
2152          <xsl:apply-templates select="*[2]">
2153           <xsl:with-param name="current_indent" select="$current_indent"/>
2154          </xsl:apply-templates>
2155         </xsl:otherwise>
2156        </xsl:choose>
2157        <br/>
2158        <xsl:call-template name="make_indent">
2159         <xsl:with-param name="current_indent" select="$current_indent"/>
2160        </xsl:call-template>
2161        <FONT color="red">Let&#x00a0;</FONT>
2162        <xsl:apply-templates mode="inline" select="*[3]"/>
2163        :
2164        <xsl:apply-templates mode="inline" select="*[4]"/>
2165        <FONT color="red">&#x00a0;such that</FONT>
2166        <br/>
2167        <xsl:call-template name="make_indent">
2168         <xsl:with-param name="current_indent" select="$current_indent"/>
2169        </xsl:call-template>
2170        (
2171        <xsl:apply-templates mode="inline" select="*[5]"/>
2172        )
2173        <xsl:apply-templates select="*[6]">
2174         <xsl:with-param name="current_indent" select="$current_indent +7"/>
2175        </xsl:apply-templates>
2176        <br/>
2177        <xsl:call-template name="make_indent">
2178         <xsl:with-param name="current_indent" select="$current_indent"/>
2179        </xsl:call-template>
2180        <xsl:apply-templates select="*[7]">
2181         <xsl:with-param name="current_indent" select="$current_indent"/>
2182        </xsl:apply-templates>
2183       </xsl:when>
2184      </xsl:choose>
2185 </xsl:template>
2186
2187 <!-- LAMBDA -->
2188
2189 <xsl:template match="m:lambda">
2190 <xsl:param name="current_indent" select="0"/>
2191     <xsl:variable name="charlength">
2192      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
2193      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
2194     </xsl:variable>
2195     <!-- <xsl:value-of select="$charlength"/> -->
2196     <!-- <xsl:value-of select="$current_indent"/> -->
2197      <xsl:choose>
2198      <xsl:when test="$charlength > $framewidth">
2199        <!-- &#x03bb; -->
2200        <xsl:call-template name="mksymbol">
2201         <xsl:with-param name="symbol" select="$lambda"/>
2202         <xsl:with-param name="color" select="'red'"/>
2203         <xsl:with-param name="size" select="'+2'"/>
2204        </xsl:call-template>
2205        <xsl:apply-templates select="m:bvar/m:ci"/>
2206        <xsl:text>:</xsl:text>
2207        <xsl:apply-templates select="m:bvar/m:type">
2208         <xsl:with-param name="current_indent"
2209            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
2210        </xsl:apply-templates><br/>
2211        <xsl:call-template name="make_indent">
2212         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2213        </xsl:call-template>
2214        <xsl:text>.</xsl:text>
2215        <xsl:apply-templates select="*[position()=2]">
2216         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2217        </xsl:apply-templates>
2218      </xsl:when>
2219      <xsl:otherwise>
2220       <xsl:apply-templates mode="inline" select="."/>
2221      </xsl:otherwise>
2222      </xsl:choose>
2223 </xsl:template>
2224
2225 <!-- href -->
2226 <xsl:template match="m:ci">
2227  <xsl:choose>
2228   <xsl:when test="boolean(@definitionURL)">
2229    <a href="{@definitionURL}">
2230    <xsl:apply-templates/>
2231    </a>
2232   </xsl:when>
2233   <xsl:otherwise>
2234    <xsl:value-of select="."/>
2235   </xsl:otherwise>
2236  </xsl:choose>
2237 </xsl:template>
2238
2239 <!-- CHAR COUNTING -->
2240
2241 <!-- enter this counting mode selecting the root -->
2242 <xsl:template match="*" mode="root_charcount">
2243 <xsl:param name="incurrent_length" select="0"/>
2244  <xsl:choose>
2245   <xsl:when test="count(*)=0">
2246    <xsl:value-of select="0"/>
2247   </xsl:when>
2248   <xsl:when test="name()='m:ci'">
2249    <xsl:value-of select="string-length()"/>
2250   </xsl:when>
2251   <xsl:otherwise>
2252    <xsl:apply-templates select="*[1]" mode="charcount">
2253     <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
2254    </xsl:apply-templates>
2255   </xsl:otherwise>
2256  </xsl:choose>
2257 </xsl:template>
2258
2259
2260         <!-- CASI PARTICOLARI MODE=INLINE -->
2261
2262 <xsl:template mode="inline" match="m:interval">
2263         <FONT color="blue">
2264         <xsl:text>[</xsl:text>
2265         </FONT>
2266         <xsl:apply-templates select="*[1]"/>
2267         <xsl:text>, </xsl:text>
2268         <xsl:apply-templates select="*[2]"/>
2269         <FONT color="blue">
2270         <xsl:text>]</xsl:text>
2271         </FONT>
2272 </xsl:template>
2273
2274 <xsl:template mode="inline" match="m:apply[m:in]">
2275         <xsl:apply-templates select="*[2]"/>
2276         <xsl:text> </xsl:text>
2277         <xsl:call-template name="mksymbol">
2278                 <xsl:with-param name="symbol" select="$member"/>
2279                 <xsl:with-param name="color" select="'blue'"/>
2280                 <xsl:with-param name="size" select="'+0'"/>
2281         </xsl:call-template>
2282         <xsl:text> </xsl:text>
2283         <xsl:apply-templates select="*[3]"/>
2284 </xsl:template>
2285
2286 <xsl:template mode="inline" match="m:integers">
2287         <xsl:call-template name="mksymbol">
2288                 <xsl:with-param name="symbol" select="$integers"/>
2289                 <xsl:with-param name="color" select="'blue'"/>
2290                 <xsl:with-param name="size" select="'+0'"/>
2291         </xsl:call-template>
2292 </xsl:template>
2293
2294 <xsl:template mode="inline" match="m:naturalnumbers">
2295         <xsl:call-template name="mksymbol">
2296                 <xsl:with-param name="symbol" select="$naturalnumbers"/>
2297                 <xsl:with-param name="size" select="'+0'"/>
2298         </xsl:call-template>
2299 </xsl:template>
2300
2301 <xsl:template mode="inline" match="m:apply[m:implies]">
2302         <xsl:text>(</xsl:text>
2303         <xsl:apply-templates select="*[2]"/>
2304         <xsl:text> </xsl:text>
2305         <xsl:call-template name="mksymbol">
2306                 <xsl:with-param name="symbol" select="$implies"/>
2307                 <xsl:with-param name="color" select="'blue'"/>
2308                 <xsl:with-param name="size" select="'+0'"/>
2309         </xsl:call-template>
2310         <xsl:text> </xsl:text>
2311         <xsl:apply-templates select="*[3]"/>
2312         <xsl:text>)</xsl:text>
2313 </xsl:template>
2314
2315 <xsl:template mode="inline" match="m:apply[m:exists]">
2316                <xsl:call-template name="mksymbol">
2317                 <xsl:with-param name="symbol" select="$NUPRLexists"/>
2318                 <xsl:with-param name="color" select="'blue'"/>
2319                 <xsl:with-param name="size" select="'+0'"/>
2320         </xsl:call-template>
2321         <xsl:apply-templates select="m:bvar/m:ci"/>
2322         <xsl:text>:</xsl:text>
2323          <xsl:apply-templates select="m:condition/*"/>
2324 <!-- CSC: old wrong code
2325         <xsl:if test="count(m:condition/m:apply/*[3]) > 1">
2326                 <xsl:text>(</xsl:text>
2327         </xsl:if>
2328         <xsl:apply-templates select="m:condition/m:apply/*[3]"/>
2329         <xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
2330                 <xsl:text>)</xsl:text>
2331         </xsl:if>
2332 -->
2333         <xsl:text>.</xsl:text>
2334         <xsl:apply-templates select="*[position()=4]"/>
2335
2336
2337 </xsl:template>
2338 <!--
2339 <xsl:template mode="inline" match="m:apply/*[m:ci][position()=1]">
2340         <xsl:apply-templates select="*[1]"/>
2341         <xsl:text>(</xsl:text>
2342         <xsl:for-each select="*[position()>1 and position()!=last()]">
2343                 <xsl:apply-templates/>
2344                 <xsl:text>, </xsl:text>
2345         </xsl:for-each>
2346         <xsl:apply-templates select="*[position()=last()]"/>
2347         <xsl:text>)</xsl:text>
2348 </xsl:template>
2349 -->
2350 <!-- CASI PARTICOLARI NON IN LINE -->
2351
2352 <xsl:template match="m:interval">
2353         <FONT color="blue">
2354         <xsl:text>[</xsl:text>
2355         </FONT>
2356         <xsl:apply-templates select="*[1]"/>
2357         <xsl:text>, </xsl:text>
2358         <xsl:apply-templates select="*[2]"/>
2359         <FONT color="blue">
2360         <xsl:text>]</xsl:text>
2361         </FONT>
2362
2363
2364  <!--<xsl:param name="current_indent" select="0"/>
2365         <xsl:variable name="charlength">
2366          <xsl:apply-templates select="." mode="charcount"/>
2367         </xsl:variable>
2368         <xsl:choose>
2369         <xsl:when test="$charlength > $framewidth">
2370         <FONT color="blue">
2371         <xsl:text>[</xsl:text>
2372         </FONT>
2373         <xsl:apply-templates select="*[1]">
2374          <xsl:with-param name="current_indent" select="$current_indent"/>
2375         </xsl:apply-templates>
2376         <xsl:text>, </xsl:text>
2377         <br/>
2378         <xsl:call-template name="make_indent">
2379          <xsl:with-param name="current_indent" select="$current_indent"/>
2380         </xsl:call-template>
2381         <xsl:apply-templates select="*[2]">
2382          <xsl:with-param name="current_indent" select="$current_indent"/>
2383         </xsl:apply-templates>
2384         <FONT color="blue">
2385         <xsl:text>]</xsl:text>
2386         </FONT>
2387         </xsl:when>
2388         <xsl:otherwise>
2389         </xsl:otherwise>
2390         </xsl:choose>-->
2391 </xsl:template>
2392
2393 <xsl:template match="m:apply[m:in]">
2394  <xsl:param name="current_indent" select="0"/>
2395         <xsl:variable name="charlength">
2396          <xsl:apply-templates select="m:in" mode="charcount"/>
2397         </xsl:variable>
2398         <xsl:choose>
2399         <xsl:when test="$charlength > $framewidth">
2400         <xsl:apply-templates select="*[2]">
2401          <xsl:with-param name="current_indent" select="$current_indent"/>
2402         </xsl:apply-templates>
2403         <br/>
2404         <xsl:call-template name="make_indent">
2405          <xsl:with-param name="current_indent" select="$current_indent"/>
2406         </xsl:call-template>
2407         <xsl:call-template name="mksymbol">
2408                 <xsl:with-param name="symbol" select="$member"/>
2409                 <xsl:with-param name="color" select="'blue'"/>
2410                 <xsl:with-param name="size" select="'+0'"/>
2411         </xsl:call-template>
2412         <xsl:text> </xsl:text>
2413         <xsl:apply-templates select="*[3]">
2414          <xsl:with-param name="current_indent" select="$current_indent"/>
2415         </xsl:apply-templates>
2416         </xsl:when>
2417         <xsl:otherwise>
2418          <xsl:apply-templates mode="inline" select="."/>
2419         </xsl:otherwise>
2420         </xsl:choose>
2421 </xsl:template>
2422
2423 <xsl:template match="m:integers">
2424         <xsl:call-template name="mksymbol">
2425                 <xsl:with-param name="symbol" select="$integers"/>
2426                 <xsl:with-param name="color" select="'blue'"/>
2427                 <xsl:with-param name="size" select="'+0'"/>
2428         </xsl:call-template>
2429 </xsl:template>
2430
2431 <xsl:template match="m:naturalnumbers">
2432         <xsl:call-template name="mksymbol">
2433                 <xsl:with-param name="symbol" select="$naturalnumbers"/>
2434                 <xsl:with-param name="size" select="'+0'"/>
2435         </xsl:call-template>
2436 </xsl:template>
2437
2438 <xsl:template match="m:apply[m:implies]">
2439     <xsl:param name="current_indent" select="0"/>
2440         <xsl:variable name="charlength">
2441          <xsl:apply-templates select="m:implies" mode="charcount"/>
2442         </xsl:variable>
2443         <xsl:choose>
2444         <xsl:when test="$charlength > $framewidth">
2445                         <xsl:text>implies</xsl:text>
2446         <xsl:text>(</xsl:text>
2447         <xsl:apply-templates select="*[2]">
2448          <xsl:with-param name="current_indent" select="$current_indent"/>
2449         </xsl:apply-templates>
2450         <br/>
2451         <xsl:call-template name="make_indent">
2452          <xsl:with-param name="current_indent" select="$current_indent"/>
2453         </xsl:call-template>
2454         <xsl:call-template name="mksymbol">
2455                 <xsl:with-param name="symbol" select="$implies"/>
2456                 <xsl:with-param name="color" select="'blue'"/>
2457                 <xsl:with-param name="size" select="'+0'"/>
2458         </xsl:call-template>
2459         <xsl:text> </xsl:text>
2460         <xsl:apply-templates select="*[3]">
2461          <xsl:with-param name="current_indent" select="$current_indent"/>
2462         </xsl:apply-templates>
2463         <xsl:text>)</xsl:text>
2464         </xsl:when>
2465         <xsl:otherwise>
2466          <xsl:apply-templates mode="inline" select="."/>
2467         </xsl:otherwise>
2468         </xsl:choose>
2469 </xsl:template>
2470
2471 <xsl:template  match="m:apply[m:exists]">
2472   <xsl:param name="current_indent" select="0"/>
2473         <xsl:variable name="charlength">
2474          <xsl:apply-templates select="m:implies" mode="charcount"/>
2475         </xsl:variable>
2476         <xsl:choose>
2477         <xsl:when test="$charlength > $framewidth">
2478         <xsl:call-template name="mksymbol">
2479                 <xsl:with-param name="symbol" select="$NUPRLexists"/>
2480                 <xsl:with-param name="color" select="'blue'"/>
2481                 <xsl:with-param name="size" select="'+0'"/>
2482         </xsl:call-template>
2483         <xsl:apply-templates select="m:bvar/m:ci"/>
2484         <xsl:text>:</xsl:text>
2485         <!--<xsl:if test="count(m:condition/m:apply/*[3]) > 1">
2486                 <xsl:text>(</xsl:text>
2487         </xsl:if>-->
2488         <xsl:apply-templates select="m:condition/m:apply/*[3]">
2489          <xsl:with-param name="current_indent" select="$current_indent"/>
2490         </xsl:apply-templates>
2491         <!--<xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
2492                 <xsl:text>)</xsl:text>
2493         </xsl:if>-->
2494         <br/>
2495         <xsl:call-template name="make_indent">
2496          <xsl:with-param name="current_indent" select="$current_indent"/>
2497         </xsl:call-template>
2498         <xsl:text>.</xsl:text>
2499         <xsl:apply-templates select="*[position()=4]">
2500          <xsl:with-param name="current_indent" select="$current_indent"/>
2501         </xsl:apply-templates>
2502         </xsl:when>
2503         <xsl:otherwise>
2504          <xsl:apply-templates mode="inline" select="."/>
2505         </xsl:otherwise>
2506         </xsl:choose>
2507 </xsl:template>
2508
2509 <!--
2510 <xsl:template match="m:apply/m:ci">
2511         <xsl:apply-templates/>
2512         <xsl:text>(</xsl:text>
2513         <xsl:for-each select="*[position()>1 and position()!=last()]">
2514                 <xsl:apply-templates/>
2515                 <xsl:text>, </xsl:text>
2516         </xsl:for-each>
2517         <xsl:apply-templates select="*[position()=last()]"/>
2518         <xsl:text>)</xsl:text>
2519 </xsl:template>
2520 -->
2521 <!-- enter this mode selecting the first child -->
2522
2523 <xsl:template match="m:ci|m:csymbol|m:implies|m:exists|m:interval|m:in" mode="charcount">
2524 <xsl:param name="incurrent_length" select="0"/>
2525     <xsl:choose>
2526     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
2527      <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>
2528      <xsl:choose>
2529      <xsl:when test="string($siblength) = &quot;&quot;">
2530       <xsl:value-of select="$incurrent_length + string-length()"/>
2531      </xsl:when>
2532      <xsl:otherwise>
2533       <xsl:value-of select="number($siblength)"/>
2534      </xsl:otherwise>
2535      </xsl:choose>
2536     </xsl:when>
2537     <xsl:otherwise>
2538      <xsl:value-of select="$incurrent_length + string-length()"/>
2539     </xsl:otherwise>
2540     </xsl:choose>
2541 </xsl:template>
2542
2543 <xsl:template match="*" mode="charcount">
2544  <xsl:param name="incurrent_length" select="0"/>
2545  <xsl:choose>
2546   <xsl:when test="count(child::*) = 0">
2547    <xsl:value-of select="$incurrent_length"/>
2548   </xsl:when>
2549   <xsl:otherwise>
2550     <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>
2551     <xsl:choose>
2552      <xsl:when test="$framewidth >= number($childlength)">
2553       <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>
2554       <xsl:choose>
2555        <xsl:when test="string($siblength) = &quot;&quot;">
2556         <xsl:value-of select="number($childlength)"/>
2557        </xsl:when>
2558        <xsl:otherwise>
2559         <xsl:value-of select="number($siblength)"/>
2560        </xsl:otherwise>
2561       </xsl:choose>
2562      </xsl:when>
2563      <xsl:otherwise>
2564       <xsl:value-of select="number($childlength)"/>
2565      </xsl:otherwise>
2566     </xsl:choose>
2567   </xsl:otherwise>
2568  </xsl:choose>
2569 </xsl:template>
2570
2571
2572 <!--***********************************************************************-->
2573 <!-- OBJECTS                                                               -->
2574 <!--***********************************************************************-->
2575
2576 <!-- Rule -->
2577
2578 <xsl:template match="Rule">
2579 <xsl:param name="current_indent" select="0"/>
2580
2581     <xsl:variable name="char">
2582      <xsl:value-of select="m:apply"/>
2583     </xsl:variable>
2584     <xsl:variable name="length" select="string-length($char)"/>
2585
2586 <p>
2587 <xsl:call-template name="make_indent">
2588         <xsl:with-param name="current_indent" select="$current_indent"/>
2589        </xsl:call-template>
2590 <FONT color="red">Rule: </FONT>
2591 <xsl:choose>
2592         <xsl:when test="m:ci">
2593                 <FONT color="red">
2594                 <xsl:apply-templates>
2595                  <xsl:with-param name="current_indent" select="$current_indent"/>
2596                 </xsl:apply-templates>
2597                 </FONT>
2598         </xsl:when>
2599         <xsl:otherwise>
2600                 <xsl:choose>
2601                 <xsl:when test="$length > $framewidth">
2602                 <br/>
2603                 <xsl:call-template name="make_indent">
2604                  <xsl:with-param name="current_indent" select="$current_indent"/>
2605                 </xsl:call-template>
2606                 <xsl:variable name="char_rule">
2607                  <xsl:value-of select="m:apply/*[1]"/>
2608                 </xsl:variable>
2609                 <xsl:variable name="length_rule" select="string-length($char_rule)"/>
2610                 <FONT>
2611                  <xsl:apply-templates select="m:apply/*[1]">
2612                   <xsl:with-param name="current_indent" select="$current_indent"/>
2613                  </xsl:apply-templates>
2614                  <xsl:if test="count(m:apply/*)>2">
2615                  <br/>
2616                  <xsl:call-template name="make_indent">
2617                   <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
2618                  </xsl:call-template>
2619                  </xsl:if>
2620                  <FONT color="red">
2621                   <xsl:text> ( </xsl:text>
2622                  </FONT>
2623                 </FONT>
2624                 <xsl:for-each select="m:apply/*[position()!=1]">
2625                 <xsl:if test="position()!=1">
2626                 <xsl:call-template name="make_indent">
2627                  <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
2628                 </xsl:call-template>
2629                 </xsl:if>
2630                 <xsl:choose>
2631                         <xsl:when test="*[1]='level-exp'">
2632                                 <xsl:text>level-exp(</xsl:text>
2633                                 <xsl:apply-templates select="*[2]">
2634                                  <xsl:with-param name="current_indent" select="$current_indent"/>
2635                                 </xsl:apply-templates>
2636                                 <xsl:text>)</xsl:text>
2637                         </xsl:when>
2638                         <xsl:when test="m:apply">
2639                                 <xsl:apply-templates select=".">
2640                                  <xsl:with-param name="current_indent" select="$current_indent"/>
2641                                 </xsl:apply-templates>
2642                         </xsl:when>
2643                         <xsl:otherwise>
2644                          <xsl:apply-templates>
2645                           <xsl:with-param name="current_indent" select="$current_indent"/>
2646                          </xsl:apply-templates>
2647                         </xsl:otherwise>
2648                 </xsl:choose>
2649                 <xsl:if test="position()!=last()">
2650                         <xsl:text>, </xsl:text>
2651                         <br/>
2652                 </xsl:if>
2653                 </xsl:for-each>
2654                 <FONT color="red">
2655                 <xsl:text> )</xsl:text>
2656                 </FONT>
2657
2658                 </xsl:when>
2659                 <xsl:otherwise>
2660                 <FONT>
2661                 <xsl:apply-templates select="m:apply/*[1]">
2662                  <xsl:with-param name="current_indent" select="$current_indent"/>
2663                 </xsl:apply-templates>
2664
2665                 <FONT color="red">
2666                 <xsl:text> ( </xsl:text>
2667                 </FONT>
2668                 </FONT>
2669                 <xsl:for-each select="m:apply/*[position()!=1]">
2670                 <xsl:choose>
2671                         <xsl:when test="*[1]='level-exp'">
2672                                 <xsl:text>level-exp(</xsl:text>
2673                                 <xsl:apply-templates select="*[2]">
2674                                  <xsl:with-param name="current_indent" select="$current_indent"/>
2675                                 </xsl:apply-templates>
2676                                 <xsl:text>)</xsl:text>
2677                         </xsl:when>
2678                         <xsl:when test="m:apply">
2679                                 <xsl:apply-templates select=".">
2680                                  <xsl:with-param name="current_indent" select="$current_indent"/>
2681                                 </xsl:apply-templates>
2682
2683                         </xsl:when>
2684                         <xsl:otherwise>
2685                                 <xsl:apply-templates>
2686                                  <xsl:with-param name="current_indent" select="$current_indent"/>
2687                                 </xsl:apply-templates>
2688                         </xsl:otherwise>
2689                 </xsl:choose>
2690                 <xsl:if test="position()!=last()">
2691                         <xsl:text>, </xsl:text>
2692                 </xsl:if>
2693                 </xsl:for-each>
2694                 <FONT color="red">
2695                 <xsl:text> )</xsl:text>
2696                 </FONT>
2697                 </xsl:otherwise>
2698                 </xsl:choose>
2699         </xsl:otherwise>
2700 </xsl:choose>
2701 </p>
2702 </xsl:template>
2703
2704 <!-- Sequent -->
2705
2706 <xsl:template match="Sequent">
2707 <xsl:param name="current_indent" select="0"/>
2708 <xsl:call-template name="make_indent">
2709  <xsl:with-param name="current_indent" select="$current_indent"/>
2710 </xsl:call-template>
2711 <FONT color="red">Sequent <xsl:value-of select="@id"/></FONT>
2712 <br/>
2713 <br/>
2714 <xsl:for-each select="Decl">
2715         <xsl:variable name="num" select="position()"/>
2716         <xsl:call-template name="make_indent">
2717          <xsl:with-param name="current_indent" select="$current_indent"/>
2718         </xsl:call-template>
2719         <xsl:value-of select="$num"/>
2720         <xsl:text>) </xsl:text>
2721                 <xsl:if test="@name">
2722                         <FONT color="green">
2723                         <xsl:value-of select="@name"/>
2724                         <xsl:text>:</xsl:text>
2725                         </FONT>
2726                 </xsl:if>
2727
2728                 <xsl:apply-templates>
2729                  <xsl:with-param name="current_indent" select="$current_indent + 10"/>
2730                 </xsl:apply-templates>
2731         <!--<xsl:choose>
2732                 <xsl:when test="m:apply">
2733                         <xsl:apply-templates select=".">
2734                          <xsl:with-param name="current_indent" select="$current_indent"/>
2735                         </xsl:apply-templates>
2736                 </xsl:when>
2737                 <xsl:otherwise>
2738                         <xsl:apply-templates>
2739                          <xsl:with-param name="current_indent" select="$current_indent"/>
2740                         </xsl:apply-templates>
2741                 </xsl:otherwise>
2742         </xsl:choose>-->
2743 <br/>
2744  </xsl:for-each>
2745  <xsl:call-template name="make_indent">
2746   <xsl:with-param name="current_indent" select="$current_indent"/>
2747  </xsl:call-template>
2748
2749  <FONT color="red" size="+1">|- </FONT>
2750  <br/>
2751  <xsl:call-template name="make_indent">
2752   <xsl:with-param name="current_indent" select="$current_indent"/>
2753  </xsl:call-template>
2754  <xsl:apply-templates select="Goal/*">
2755   <xsl:with-param name="current_indent" select="$current_indent"/>
2756  </xsl:apply-templates>
2757 </xsl:template>
2758
2759 <!-- NODE -->
2760
2761 <xsl:template match="Node">
2762  <xsl:param name="current_indent" select="0"/>
2763
2764        <xsl:variable name="nonce" select="generate-id()"/>
2765        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
2766        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
2767        <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
2768        <xsl:variable name="freshid5" select="concat('e',$nonce)"/>
2769        <br/>
2770        <xsl:apply-templates select="Sequent">
2771         <xsl:with-param name="current_indent" select="$current_indent"/>
2772        </xsl:apply-templates>
2773        <xsl:choose>
2774         <xsl:when test="Rule">
2775          <xsl:apply-templates select="Rule">
2776           <xsl:with-param name="current_indent" select="$current_indent"/>
2777          </xsl:apply-templates>
2778         </xsl:when>
2779         <xsl:when test="TacticInstance">
2780          <br/>
2781          <br/>
2782          <span>
2783           <xsl:call-template name="make_indent">
2784            <xsl:with-param name="current_indent" select="$current_indent"/>
2785           </xsl:call-template>
2786           <xsl:text>By </xsl:text>
2787           <xsl:apply-templates select="TacticInstance/@name"/>
2788           <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
2789           <xsl:if test="$explode_tactics">
2790            <span ID="{$freshid4}">
2791             <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid4}'));Show(document.getElementById('{$freshid5}'));return (0==1);">Details</a>
2792            </span>
2793           </xsl:if>
2794          </span>
2795          <xsl:if test="$explode_tactics">
2796           <div ID="{$freshid5}">
2797            <xsl:call-template name="make_indent">
2798             <xsl:with-param name="current_indent" select="$current_indent"/>
2799            </xsl:call-template>
2800            <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid4}'));Hide(document.getElementById('{$freshid5}'));return (0==1);">Hide details</a>
2801            <br/>
2802            <xsl:apply-templates select="TacticProof">
2803                  <xsl:with-param name="current_indent" select="$current_indent + 5"/>
2804            </xsl:apply-templates>
2805           </div>
2806          </xsl:if>
2807          <br/><br/>
2808         </xsl:when>
2809        </xsl:choose>
2810         <xsl:if test="count(Node)!=0">
2811             <xsl:choose>
2812             <xsl:when test="count(Node)=1">
2813             <span ID="{$freshid2}">
2814              <xsl:call-template name="make_indent">
2815               <xsl:with-param name="current_indent" select="$current_indent"/>
2816              </xsl:call-template>
2817              <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoal</a>
2818              <br/>
2819             </span>
2820             </xsl:when>
2821             <xsl:otherwise>
2822             <span ID="{$freshid2}">
2823              <xsl:call-template name="make_indent">
2824               <xsl:with-param name="current_indent" select="$current_indent"/>
2825              </xsl:call-template>
2826              <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoals</a>
2827              <br/>
2828             </span>
2829             </xsl:otherwise>
2830             </xsl:choose>
2831             <div ID="{$freshid3}">
2832              <xsl:call-template name="make_indent">
2833               <xsl:with-param name="current_indent" select="$current_indent"/>
2834              </xsl:call-template>
2835              <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid2}'));Hide(document.getElementById('{$freshid3}'));return (0==1);">Back</a>
2836              <br/>
2837              <xsl:apply-templates select="Node">
2838                 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
2839              </xsl:apply-templates>
2840             </div>
2841           <script>
2842            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
2843           </script>
2844           </xsl:if>
2845 </xsl:template>
2846
2847 <!-- NuPRLDefinition -->
2848
2849 <xsl:template match="NuPrlDefinition">
2850  <xsl:apply-templates select="*[1]"/>
2851  <xsl:text> := </xsl:text>
2852  <xsl:apply-templates select="*[2]"/>
2853 </xsl:template>
2854
2855 <!-- DEFINITION -->
2856
2857 <xsl:template match="Definition">
2858 <xsl:param name="current_indent" select="0"/>
2859 <p>
2860 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2861 TYPE =<br/>
2862       <xsl:call-template name="make_indent">
2863        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2864       </xsl:call-template>
2865        <xsl:apply-templates select="type/*[1]">
2866         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2867        </xsl:apply-templates><br/>
2868 BODY =<br/>
2869       <xsl:call-template name="make_indent">
2870        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2871       </xsl:call-template>
2872        <xsl:apply-templates select="body/Node">
2873         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2874        </xsl:apply-templates>
2875 </p>
2876 </xsl:template>
2877
2878 <!-- AXIOM -->
2879
2880 <xsl:template match="Axiom">
2881 <xsl:param name="current_indent" select="0"/>
2882 <p>
2883 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2884 TYPE =<br/>
2885       <xsl:call-template name="make_indent">
2886        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2887       </xsl:call-template>
2888 <xsl:apply-templates select="type/*[1]">
2889           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2890        </xsl:apply-templates>
2891 </p>
2892 </xsl:template>
2893
2894 <!-- UNFINISHED PROOF -->
2895
2896 <xsl:template match="CurrentProof">
2897 <xsl:param name="current_indent" select="0"/>
2898 <p>
2899 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2900 THESIS:  <xsl:apply-templates select="type/*[1]">
2901           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2902          </xsl:apply-templates><br/>
2903 CONJECTURES:
2904       <xsl:for-each select="Conjecture">
2905       <br/>
2906       <xsl:call-template name="make_indent">
2907        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2908       </xsl:call-template>
2909       <xsl:for-each select="Decl|Def|Hidden">
2910        <xsl:choose>
2911         <xsl:when test="name(.)='Decl'">
2912          <xsl:choose>
2913           <xsl:when test="@name">
2914            <xsl:value-of select="@name"/>
2915           </xsl:when>
2916           <xsl:otherwise>
2917            <xsl:text>_</xsl:text>
2918           </xsl:otherwise>
2919          </xsl:choose>
2920          <xsl:text> : </xsl:text>
2921          <xsl:apply-templates select="./*[1]">
2922           <xsl:with-param name="current_indent" select="$current_indent"/>
2923          </xsl:apply-templates>
2924         </xsl:when>
2925         <xsl:when test="name(.)='Def'">
2926          <xsl:choose>
2927           <xsl:when test="@name">
2928            <xsl:value-of select="@name"/>
2929           </xsl:when>
2930           <xsl:otherwise>
2931            <xsl:text>_</xsl:text>
2932           </xsl:otherwise>
2933          </xsl:choose>
2934          <xsl:text> := </xsl:text>
2935          <xsl:apply-templates select="./*[1]">
2936           <xsl:with-param name="current_indent" select="$current_indent"/>
2937          </xsl:apply-templates>
2938         </xsl:when>
2939         <xsl:otherwise>
2940          <xsl:text> _ :? _ </xsl:text>
2941         </xsl:otherwise>
2942        </xsl:choose>
2943       </xsl:for-each>
2944       |- <xsl:value-of select="./@no"/> :
2945       <xsl:apply-templates select="./Goal/*[1]">
2946        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
2947       </xsl:apply-templates>
2948       </xsl:for-each>
2949       <br/>
2950 PROOF:
2951       <xsl:apply-templates select="body/*[1]">
2952         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2953       </xsl:apply-templates>
2954 </p>
2955 </xsl:template>
2956
2957 <!-- MUTUAL INDUCTIVE DEFINITION -->
2958
2959 <xsl:template match="InductiveDefinition">
2960 <xsl:param name="current_indent" select="0"/>
2961 <p>
2962      <xsl:for-each select="InductiveType">
2963          <xsl:choose>
2964          <xsl:when test="position() = 1">
2965           <xsl:choose>
2966           <xsl:when test="string(./@inductive) = &quot;true&quot;">
2967           INDUCTIVE DEFINITION
2968           </xsl:when>
2969           <xsl:otherwise>
2970           COINDUCTIVE DEFINITION
2971           </xsl:otherwise>
2972           </xsl:choose>
2973          </xsl:when>
2974          <xsl:otherwise>
2975           AND
2976          </xsl:otherwise>
2977          </xsl:choose>
2978          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
2979          [
2980           <xsl:if test="string(../Param) != &quot;&quot;">
2981            <xsl:for-each select="../Param">
2982             <xsl:value-of select="./@name"/>
2983             :
2984             <xsl:apply-templates select="*"/>
2985            </xsl:for-each>
2986           </xsl:if>
2987          ] <br/>
2988          OF ARITY
2989          <xsl:apply-templates select="./arity/*[1]">
2990           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2991          </xsl:apply-templates> <br/>
2992          BUILT FROM:
2993       <xsl:for-each select="./Constructor">
2994       <br/>
2995       <xsl:call-template name="make_indent">
2996        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
2997       </xsl:call-template>
2998          <xsl:choose>
2999          <xsl:when test="position() = 1">
3000          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
3001          </xsl:when>
3002          <xsl:otherwise>
3003          <xsl:text>| </xsl:text>
3004          </xsl:otherwise>
3005          </xsl:choose>
3006          <xsl:value-of select="./@name"/>
3007          <xsl:text>: </xsl:text>
3008          <xsl:apply-templates select="./*[1]">
3009           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
3010          </xsl:apply-templates>
3011       </xsl:for-each>
3012      </xsl:for-each>
3013 </p>
3014 </xsl:template>
3015
3016 <!-- VARIABLE -->
3017
3018 <xsl:template match="Variable">
3019 <xsl:param name="current_indent" select="0"/>
3020 <p>
3021 VARIABLE <xsl:value-of select="@name"/><br/>
3022 TYPE = <xsl:apply-templates select="type/*[1]">
3023           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
3024        </xsl:apply-templates>
3025 <xsl:if test="body">
3026 <br/>
3027 BODY = <xsl:apply-templates select="body/*[1]">
3028           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
3029        </xsl:apply-templates>
3030 </xsl:if>
3031 </p>
3032 </xsl:template>
3033
3034 <!--***********************************************************************-->
3035 <!-- SECTIONS                                                              -->
3036 <!--***********************************************************************-->
3037
3038 <!-- SECTION -->
3039
3040 <xsl:template match="SECTION">
3041 <xsl:param name="current_indent" select="0"/>
3042  <h1>BEGIN OF SECTION</h1>
3043   <xsl:apply-templates/>
3044  <h1>END OF SECTION</h1>
3045 </xsl:template>
3046
3047 </xsl:stylesheet>