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:value-of select="concat(string($absPath), @definitionURL)"/>
 114   </xsl:variable>-->
 115   <xsl:choose>
 116    <xsl:when test="count(child::*) = 0">
 117     <xsl:call-template name="mksymbol">
 118      <xsl:with-param name="symbol" select="'emptyset'"/>
 119     </xsl:call-template>
 120    </xsl:when>
 121    <xsl:otherwise>
 122     <xsl:choose>
 123      <xsl:when test="name(*[1]) = 'm:bvar'">
 124       <xsl:text>{</xsl:text>
 125       <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 126       <xsl:text>:</xsl:text>
 127       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 128       <xsl:text>|</xsl:text>
 129       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 130       <xsl:text>}</xsl:text>
 131      </xsl:when>
 132      <xsl:otherwise>
 133       <xsl:text>{</xsl:text>
 134       <xsl:for-each select="*">
 135        <xsl:apply-templates mode="inline" select="."/>
 136        <xsl:choose>
 137         <xsl:when test="position() = last()">
 138          <xsl:text>}</xsl:text>
 139         </xsl:when>
 140         <xsl:otherwise>
 141          <xsl:text>,</xsl:text>
 142         </xsl:otherwise>
 143        </xsl:choose>
 144       </xsl:for-each>
 145      </xsl:otherwise>
 146     </xsl:choose>
 147    </xsl:otherwise>
 148   </xsl:choose>
 149  </xsl:template>
 150
 151
 152 <!-- CARD -->
 153 <xsl:template mode="inline" match="m:apply[m:card]">
 154   <xsl:param name="current_indent" select="0"/>
 155   <xsl:param name="width" select="$framewidth"/>
 156   <xsl:variable name="uri">
 157    <xsl:value-of select="m:card/@definitionURL"/>
 158   </xsl:variable>
 159   <xsl:text>|</xsl:text>
 160   <xsl:apply-templates mode="inline" select="*[2]"/>
 161   <xsl:text>|</xsl:text>
 162  </xsl:template>
 163
 164 <xsl:template mode="inline" match="m:apply[m:in|m:notin|m:intersect|m:union
 165   |m:subset|m:prsubset|m:setdiff]">
 166   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 167   <xsl:variable name="symbol">
 168    <xsl:choose>
 169     <xsl:when test="m:in">
 170      <xsl:value-of select="'&#206;'"/>
 171     </xsl:when>
 172     <xsl:when test="m:notin">
 173      <xsl:value-of select="'&#207;'"/>
 174     </xsl:when>
 175     <xsl:when test="m:intersect">
 176      <xsl:value-of select="'&#199;'"/>
 177     </xsl:when>
 178     <xsl:when test="m:union">
 179      <xsl:value-of select="'&#200;'"/>
 180     </xsl:when>
 181     <xsl:when test="m:subset">
 182      <xsl:value-of select="'&#205;'"/>
 183     </xsl:when>
 184     <xsl:when test="m:prsubset">
 185      <xsl:value-of select="'&#204;'"/>
 186     </xsl:when>
 187     <xsl:when test="m:setdiff">
 188      <xsl:value-of select="'/'"/>
 189     </xsl:when>
 190    </xsl:choose>
 191   </xsl:variable>
 192   <xsl:text>(</xsl:text>
 193   <xsl:apply-templates mode="inline" select="*[2]"/>
 194   <xsl:choose>
 195   <xsl:when test="$uri != ''">
 196    <a href="{$uri}">
 197     <xsl:call-template name="mksymbol">
 198      <xsl:with-param name="symbol">
 199       <xsl:value-of select="local-name(*[1])"/>
 200      </xsl:with-param>
 201     </xsl:call-template>
 202    </a>
 203   </xsl:when>
 204   <xsl:otherwise>
 205     <xsl:call-template name="mksymbol">
 206      <xsl:with-param name="symbol">
 207       <xsl:value-of select="local-name(*[1])"/>
 208      </xsl:with-param>
 209     </xsl:call-template>
 210   </xsl:otherwise>
 211   </xsl:choose>
 212   <xsl:apply-templates mode="inline" select="*[3]"/>
 213   <xsl:text>)</xsl:text>
 214  </xsl:template>
 215
 216 <!-- *************************************************************** -->
 217
 218 <xsl:template match="m:apply[m:in|m:notin|m:intersect|m:union
 219   |m:subset|m:prsubset|m:setdiff]">
 220   <xsl:param name="current_indent" select="0"/>
 221   <xsl:param name="width" select="$framewidth"/>
 222   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 223   <xsl:variable name="charlength">
 224    <xsl:apply-templates select="*[1]" mode="charcount"/>
 225   </xsl:variable>
 226   <xsl:variable name="symbol">
 227    <xsl:choose>
 228     <xsl:when test="m:in">
 229      <xsl:value-of select="'&#206;'"/>
 230     </xsl:when>
 231     <xsl:when test="m:notin">
 232      <xsl:value-of select="'&#207;'"/>
 233     </xsl:when>
 234     <xsl:when test="m:intersect">
 235      <xsl:value-of select="'&#199;'"/>
 236     </xsl:when>
 237     <xsl:when test="m:union">
 238      <xsl:value-of select="'&#200;'"/>
 239     </xsl:when>
 240     <xsl:when test="m:subset">
 241      <xsl:value-of select="'&#205;'"/>
 242     </xsl:when>
 243     <xsl:when test="m:prsubset">
 244      <xsl:value-of select="'&#204;'"/>
 245     </xsl:when>
 246     <xsl:when test="m:setdiff">
 247      <xsl:value-of select="'/'"/>
 248     </xsl:when>
 249    </xsl:choose>
 250   </xsl:variable>
 251   <xsl:choose>
 252     <xsl:when test="$charlength > $framewidth">
 253      <xsl:text>(</xsl:text>
 254      <xsl:apply-templates select="*[2]">
 255       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 256      </xsl:apply-templates>
 257      <BR/>
 258      <xsl:call-template name="make_indent">
 259       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 260      </xsl:call-template>
 261      <xsl:choose>
 262      <xsl:when test="$uri != ''">
 263       <a href="{$uri}">
 264        <xsl:call-template name="mksymbol">
 265         <xsl:with-param name="symbol">
 266          <xsl:value-of select="local-name(*[1])"/>
 267         </xsl:with-param>
 268        </xsl:call-template>
 269       </a>
 270      </xsl:when>
 271      <xsl:otherwise>
 272        <xsl:call-template name="mksymbol">
 273         <xsl:with-param name="symbol">
 274          <xsl:value-of select="local-name(*[1])"/>
 275         </xsl:with-param>
 276        </xsl:call-template>
 277      </xsl:otherwise>
 278      </xsl:choose>
 279      <xsl:apply-templates select="*[3]">
 280       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 281      </xsl:apply-templates>
 282      <xsl:text>)</xsl:text>
 283     </xsl:when>
 284     <xsl:otherwise>
 285      <xsl:apply-templates mode="inline" select="."/>
 286     </xsl:otherwise>
 287    </xsl:choose>
 288  </xsl:template>
 289
 290
 291 <!-- SET -->
 292
 293  <xsl:template match="m:set">
 294   <xsl:param name="current_indent" select="0"/>
 295   <xsl:param name="width" select="$framewidth"/>
 296   <xsl:variable name="uri" select="@definitionURL"/>
 297 <!--   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
 298   </xsl:variable>-->
 299   <xsl:choose>
 300    <xsl:when test="count(child::*) = 0">
 301     <xsl:call-template name="mksymbol">
 302      <xsl:with-param name="symbol" select="'emptyset'"/>
 303     </xsl:call-template>
 304    </xsl:when>
 305    <xsl:otherwise>
 306     <xsl:variable name="charlength">
 307      <xsl:apply-templates select="." mode="charcount"/>
 308     </xsl:variable>
 309     <xsl:choose>
 310      <xsl:when test="$charlength > $framewidth">
 311       <xsl:choose>
 312        <xsl:when test="name(*[1]) = 'm:bvar'">
 313         <xsl:text>{</xsl:text>
 314         <xsl:apply-templates select="m:bvar/m:ci"/>
 315         <xsl:text>:</xsl:text>
 316         <xsl:apply-templates select="m:bvar/m:type">
 317          <xsl:with-param name="current_indent"
 318            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 319         </xsl:apply-templates><BR/>
 320         <xsl:call-template name="make_indent">
 321          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 322         </xsl:call-template>
 323         <xsl:text>|</xsl:text>
 324         <xsl:apply-templates select="m:condition">
 325          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 326         </xsl:apply-templates>
 327         <xsl:text>}</xsl:text>
 328        </xsl:when>
 329        <xsl:otherwise>
 330         <xsl:text>{</xsl:text>
 331          <xsl:apply-templates select="*[position()=1]">
 332           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 333          </xsl:apply-templates>
 334          <xsl:for-each select="*[position()>1]">
 335           <xsl:text>,</xsl:text>
 336           <BR/>
 337           <xsl:call-template name="make_indent">
 338            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 339           </xsl:call-template>
 340           <xsl:apply-templates select=".">
 341            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 342           </xsl:apply-templates>
 343          </xsl:for-each>
 344         <xsl:text>}</xsl:text>
 345        </xsl:otherwise>
 346       </xsl:choose>
 347      </xsl:when>
 348      <xsl:otherwise>
 349       <xsl:apply-templates mode="inline" select="."/>
 350      </xsl:otherwise>
 351     </xsl:choose>
 352    </xsl:otherwise>
 353   </xsl:choose>
 354  </xsl:template>
 355
 356 <!-- CARD -->
 357 <xsl:template match="m:apply[m:card]">
 358   <xsl:param name="current_indent" select="0"/>
 359   <xsl:param name="width" select="$framewidth"/>
 360   <xsl:variable name="uri">
 361    <xsl:value-of select="m:card/@definitionURL"/>
 362   </xsl:variable>
 363   <xsl:text>|</xsl:text>
 364   <xsl:apply-templates select="*[2]">
 365    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 366   </xsl:apply-templates>
 367   <xsl:text>|</xsl:text>
 368  </xsl:template>
 369
 370 <!-- COUNTING -->
 371
 372 <xsl:template match="m:in|m:notin|m:intersect|m:union
 373            |m:subset|m:prsubset|m:setdiff|m:card" mode="charcount">
 374 <xsl:param name="incurrent_length" select="0"/>
 375     <xsl:choose>
 376     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 377      <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>
 378      <xsl:choose>
 379      <xsl:when test="string($siblength) = &quot;&quot;">
 380       <xsl:value-of select="$incurrent_length + string-length()"/>
 381      </xsl:when>
 382      <xsl:otherwise>
 383       <xsl:value-of select="number($siblength)"/>
 384      </xsl:otherwise>
 385      </xsl:choose>
 386     </xsl:when>
 387     <xsl:otherwise>
 388      <xsl:value-of select="$incurrent_length + string-length()"/>
 389     </xsl:otherwise>
 390     </xsl:choose>
 391 </xsl:template>
 392
 393 </xsl:stylesheet>