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