helm/style/html_init.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 <!-- INIT style for HTML                                                   -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
  33 <!--***********************************************************************-->
  34
  35 <!-- INLINE MODE : BASIC OPERATORS -->
  36
  37  <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
  38        |m:geq|m:gt|m:plus|m:times]">
  39   <xsl:variable name="uri">
  40    <xsl:value-of select="*[1]/@definitionURL"/>
  41   </xsl:variable>
  42   <xsl:variable name="symbol">
  43    <xsl:choose>
  44     <xsl:when test="m:and">
  45      <xsl:value-of select="'&#217;'"/>
  46     </xsl:when>
  47     <xsl:when test="m:or">
  48      <xsl:value-of select="'&#218;'"/>
  49     </xsl:when>
  50     <xsl:when test="m:eq">
  51      <xsl:value-of select="'&#61;'"/>
  52     </xsl:when>
  53     <xsl:when test="m:neq">
  54      <xsl:value-of select="'&#185;'"/>
  55     </xsl:when>
  56     <xsl:when test="m:leq">
  57      <xsl:value-of select="'&#163;'"/>
  58     </xsl:when>
  59     <xsl:when test="m:lt">
  60      <xsl:value-of select="'&#60;'"/>
  61     </xsl:when>
  62     <xsl:when test="m:geq">
  63      <xsl:value-of select="'&#179;'"/>
  64     </xsl:when>
  65     <xsl:when test="m:gt">
  66      <xsl:value-of select="'&#62;'"/>
  67     </xsl:when>
  68     <xsl:when test="m:plus">
  69      <xsl:value-of select="'&#43;'"/>
  70     </xsl:when>
  71     <xsl:when test="m:times">
  72      <xsl:value-of select="'&#42;'"/>
  73     </xsl:when>
  74    </xsl:choose>
  75   </xsl:variable>
  76   <xsl:text>(</xsl:text>
  77   <xsl:apply-templates mode="inline" select="*[2]"/>
  78   <a>
  79    <xsl:attribute name="href">
  80     <xsl:call-template name="makeURL">
  81      <xsl:with-param name="url" select="$uri"/>
  82     </xsl:call-template>
  83    </xsl:attribute>
  84    <FONT FACE="symbol" mathcolor="blue">
  85     <xsl:value-of select="$symbol"/>
  86    </FONT>
  87   </a>
  88   <xsl:apply-templates mode="inline" select="*[3]"/>
  89   <xsl:text>)</xsl:text>
  90  </xsl:template>
  91
  92 <!-- INLINE MODE - MINUS (can be unary!) -->
  93
  94 <xsl:template mode="inline" match="m:apply[m:minus]">
  95   <xsl:variable name="uri">
  96    <xsl:value-of select="*[1]/@definitionURL"/>
  97   </xsl:variable>
  98   <xsl:choose>
  99    <xsl:when test="count(child::*)=2">
 100     <a>
 101     <xsl:attribute name="href">
 102     <xsl:call-template name="makeURL">
 103      <xsl:with-param name="url" select="$uri"/>
 104     </xsl:call-template>
 105     </xsl:attribute>
 106     <xsl:text>-</xsl:text>
 107     </a>
 108     <xsl:apply-templates mode="inline" select="*[2]"/>
 109    </xsl:when>
 110    <xsl:otherwise>
 111     <xsl:text>(</xsl:text>
 112     <xsl:apply-templates mode="inline" select="*[2]"/>
 113     <a>
 114      <xsl:attribute name="href">
 115       <xsl:call-template name="makeURL">
 116        <xsl:with-param name="url" select="$uri"/>
 117       </xsl:call-template>
 118      </xsl:attribute>
 119      <xsl:text>-</xsl:text>
 120     </a>
 121     <xsl:apply-templates mode="inline" select="*[3]"/>
 122     <xsl:text>)</xsl:text>
 123    </xsl:otherwise>
 124   </xsl:choose>
 125  </xsl:template>
 126
 127 <!-- INLINE MODE NOT -->
 128
 129  <xsl:template mode="inline" match="m:apply[m:not]">
 130   <xsl:variable name="uri">
 131    <xsl:value-of select="m:not/@definitionURL"/>
 132   </xsl:variable>
 133      <a>
 134      <xsl:attribute name="href">
 135       <xsl:call-template name="makeURL">
 136        <xsl:with-param name="url" select="$uri"/>
 137       </xsl:call-template>
 138      </xsl:attribute>
 139      <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
 140      </a>
 141      <xsl:apply-templates mode="inline" select="*[2]"/>
 142  </xsl:template>
 143
 144 <!-- INLINE MODE EXISTS -->
 145
 146  <xsl:template mode="inline" match="m:apply[m:exists]">
 147   <xsl:variable name="uri">
 148    <xsl:value-of select="m:exists/@definitionURL"/>
 149   </xsl:variable>
 150   <a>
 151    <xsl:attribute name="href">
 152     <xsl:call-template name="makeURL">
 153      <xsl:with-param name="url" select="$uri"/>
 154     </xsl:call-template>
 155    </xsl:attribute>
 156    <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
 157   </a>
 158   <xsl:apply-templates select="m:bvar/m:ci"/>
 159   <xsl:text>:</xsl:text>
 160   <xsl:apply-templates mode="inline" select="m:condition"/>
 161   <xsl:text>.</xsl:text>
 162   <xsl:apply-templates mode="inline" select="*[last()]"/>
 163  </xsl:template>
 164
 165 <!-- COUNTING MODE -->
 166
 167 <!-- BASIC OPERATORS -->
 168
 169  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
 170        |m:geq|m:gt|m:plus|m:times]">
 171   <xsl:param name="current_indent" select="0"/>
 172   <xsl:param name="width" select="$framewidth"/>
 173   <xsl:variable name="uri">
 174    <xsl:value-of select="*[1]/@definitionURL"/>
 175   </xsl:variable>
 176   <xsl:variable name="charlength">
 177    <xsl:apply-templates select="*[1]" mode="charcount"/>
 178   </xsl:variable>
 179   <xsl:variable name="symbol">
 180    <xsl:choose>
 181     <xsl:when test="m:and">
 182      <xsl:value-of select="'&#217;'"/>
 183     </xsl:when>
 184     <xsl:when test="m:or">
 185      <xsl:value-of select="'&#218;'"/>
 186     </xsl:when>
 187     <xsl:when test="m:eq">
 188      <xsl:value-of select="'&#61;'"/>
 189     </xsl:when>
 190     <xsl:when test="m:neq">
 191      <xsl:value-of select="'&#185;'"/>
 192     </xsl:when>
 193     <xsl:when test="m:leq">
 194      <xsl:value-of select="'&#163;'"/>
 195     </xsl:when>
 196     <xsl:when test="m:lt">
 197      <xsl:value-of select="'&#60;'"/>
 198     </xsl:when>
 199     <xsl:when test="m:geq">
 200      <xsl:value-of select="'&#179;'"/>
 201     </xsl:when>
 202     <xsl:when test="m:gt">
 203      <xsl:value-of select="'&#62;'"/>
 204     </xsl:when>
 205     <xsl:when test="m:plus">
 206      <xsl:value-of select="'&#43;'"/>
 207     </xsl:when>
 208     <xsl:when test="m:times">
 209      <xsl:value-of select="'&#42;'"/>
 210     </xsl:when>
 211    </xsl:choose>
 212   </xsl:variable>
 213   <xsl:choose>
 214     <xsl:when test="$charlength > $framewidth">
 215      <xsl:text>(</xsl:text>
 216      <xsl:apply-templates select="*[2]">
 217       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 218      </xsl:apply-templates>
 219      <BR/>
 220      <xsl:call-template name="make_indent">
 221       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 222      </xsl:call-template>
 223      <a>
 224      <xsl:attribute name="href">
 225       <xsl:call-template name="makeURL">
 226        <xsl:with-param name="url" select="$uri"/>
 227       </xsl:call-template>
 228      </xsl:attribute>
 229      <FONT FACE="symbol" mathcolor="blue">
 230       <xsl:value-of select="$symbol"/>
 231      </FONT>
 232      </a>
 233      <xsl:apply-templates select="*[3]">
 234       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 235      </xsl:apply-templates>
 236      <xsl:text>)</xsl:text>
 237     </xsl:when>
 238     <xsl:otherwise>
 239      <xsl:apply-templates mode="inline" select="."/>
 240     </xsl:otherwise>
 241    </xsl:choose>
 242  </xsl:template>
 243
 244 <!-- MINUS (can be unary!) -->
 245
 246 <xsl:template match="m:apply[m:minus]">
 247   <xsl:param name="current_indent" select="0"/>
 248   <xsl:param name="width" select="$framewidth"/>
 249   <xsl:variable name="uri">
 250    <xsl:value-of select="*[1]/@definitionURL"/>
 251   </xsl:variable>
 252   <xsl:choose>
 253    <xsl:when test="count(child::*)=2">
 254     <a>
 255     <xsl:attribute name="href">
 256      <xsl:call-template name="makeURL">
 257       <xsl:with-param name="url" select="$uri"/>
 258      </xsl:call-template>
 259     </xsl:attribute>
 260     <xsl:text>-</xsl:text>
 261     </a>
 262     <xsl:apply-templates select="*[2]">
 263      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
 264     </xsl:apply-templates>
 265    </xsl:when>
 266    <xsl:otherwise>
 267     <xsl:variable name="charlength">
 268      <xsl:apply-templates select="*[1]" mode="charcount"/>
 269     </xsl:variable>
 270     <xsl:choose>
 271      <xsl:when test="$charlength > $framewidth">
 272       <xsl:text>(</xsl:text>
 273       <xsl:apply-templates select="*[2]">
 274        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 275       </xsl:apply-templates>
 276       <BR/>
 277       <xsl:call-template name="make_indent">
 278        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 279       </xsl:call-template>
 280       <a>
 281       <xsl:attribute name="href">
 282        <xsl:call-template name="makeURL">
 283         <xsl:with-param name="url" select="$uri"/>
 284        </xsl:call-template>
 285       </xsl:attribute>
 286       <xsl:text>-</xsl:text>
 287       </a>
 288       <xsl:apply-templates select="*[3]">
 289        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 290       </xsl:apply-templates>
 291       <xsl:text>)</xsl:text>
 292      </xsl:when>
 293      <xsl:otherwise>
 294       <xsl:apply-templates mode="inline" select="."/>
 295      </xsl:otherwise>
 296     </xsl:choose>
 297    </xsl:otherwise>
 298   </xsl:choose>
 299  </xsl:template>
 300
 301 <!-- NOT -->
 302
 303  <xsl:template match="m:apply[m:not]">
 304   <xsl:param name="current_indent" select="0"/>
 305   <xsl:param name="width" select="$framewidth"/>
 306   <xsl:variable name="uri">
 307    <xsl:value-of select="m:not/@definitionURL"/>
 308   </xsl:variable>
 309      <a>
 310      <xsl:attribute name="href">
 311       <xsl:call-template name="makeURL">
 312        <xsl:with-param name="url" select="$uri"/>
 313       </xsl:call-template>
 314      </xsl:attribute>
 315      <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
 316      </a>
 317      <xsl:apply-templates select="*[2]"/>
 318  </xsl:template>
 319
 320 <!-- EXISTS -->
 321
 322  <xsl:template match="m:apply[m:exists]">
 323   <xsl:param name="current_indent" select="0"/>
 324   <xsl:param name="width" select="$framewidth"/>
 325   <xsl:variable name="uri">
 326    <xsl:value-of select="m:exists/@definitionURL"/>
 327   </xsl:variable>
 328   <xsl:variable name="charlength">
 329    <xsl:apply-templates select="m:exists" mode="charcount"/>
 330   </xsl:variable>
 331   <xsl:choose>
 332     <xsl:when test="$charlength > $framewidth">
 333      <a>
 334      <xsl:attribute name="href">
 335       <xsl:call-template name="makeURL">
 336        <xsl:with-param name="url" select="$uri"/>
 337       </xsl:call-template>
 338      </xsl:attribute>
 339      <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
 340      </a>
 341      <xsl:apply-templates select="m:bvar/m:ci"/>
 342      <xsl:text>:</xsl:text>
 343      <xsl:apply-templates select="m:condition">
 344       <xsl:with-param name="current_indent" select="$current_indent + 2 +
 345                                 string-length(bvar/ci)"/>
 346      </xsl:apply-templates>
 347      <BR/>
 348       <xsl:call-template name="make_indent">
 349        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 350       </xsl:call-template>
 351      <xsl:text>.</xsl:text>
 352       <xsl:apply-templates select="*[last()]">
 353        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 354       </xsl:apply-templates>
 355     </xsl:when>
 356     <xsl:otherwise>
 357      <xsl:apply-templates mode="inline" select="."/>
 358     </xsl:otherwise>
 359    </xsl:choose>
 360  </xsl:template>
 361
 362
 363
 364
 365 <!-- COUNTING -->
 366
 367 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
 368    |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
 369 <xsl:param name="incurrent_length" select="0"/>
 370     <xsl:choose>
 371     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 372      <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>
 373      <xsl:choose>
 374      <xsl:when test="string($siblength) = &quot;&quot;">
 375       <xsl:value-of select="$incurrent_length + string-length()"/>
 376      </xsl:when>
 377      <xsl:otherwise>
 378       <xsl:value-of select="number($siblength)"/>
 379      </xsl:otherwise>
 380      </xsl:choose>
 381     </xsl:when>
 382     <xsl:otherwise>
 383      <xsl:value-of select="$incurrent_length + string-length()"/>
 384     </xsl:otherwise>
 385     </xsl:choose>
 386 </xsl:template>
 387
 388 </xsl:stylesheet>
 389
 390