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:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
  36
  37 <!-- IN -->
  38
  39  <xsl:template match="m:apply[m:in]">
  40   <xsl:param name="current_indent" select="0"/>
  41   <xsl:param name="width" select="$framewidth"/>
  42   <xsl:variable name="uri">
  43    <xsl:value-of select="m:in/@definitionURL"/>
  44   </xsl:variable>
  45   <xsl:variable name="charlength">
  46    <xsl:apply-templates select="m:in" mode="charcount"/>
  47   </xsl:variable>
  48   <xsl:choose>
  49     <xsl:when test="$charlength > $framewidth">
  50      <xsl:text>(</xsl:text>
  51      <xsl:apply-templates select="*[2]">
  52       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
  53      </xsl:apply-templates>
  54      <BR/>
  55      <xsl:call-template name="make_indent">
  56       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
  57      </xsl:call-template>
  58      <a>
  59      <xsl:attribute name="href">
  60       <xsl:value-of select="concat(string($header),string($uri))"/>
  61      </xsl:attribute>
  62      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
  63      </a>
  64      <xsl:apply-templates select="*[3]">
  65       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
  66      </xsl:apply-templates>
  67      <xsl:text>)</xsl:text>
  68     </xsl:when>
  69     <xsl:otherwise>
  70      <xsl:text>(</xsl:text>
  71      <xsl:apply-templates select="*[2]"/>
  72      <a>
  73      <xsl:attribute name="href">
  74       <xsl:value-of select="concat(string($header),string($uri))"/>
  75      </xsl:attribute>
  76      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
  77      </a>
  78      <xsl:apply-templates select="*[3]"/>
  79      <xsl:text>)</xsl:text>
  80     </xsl:otherwise>
  81    </xsl:choose>
  82  </xsl:template>
  83
  84 <!-- NOTIN -->
  85
  86  <xsl:template match="m:apply[m:notin]">
  87   <xsl:param name="current_indent" select="0"/>
  88   <xsl:param name="width" select="$framewidth"/>
  89   <xsl:variable name="uri">
  90    <xsl:value-of select="m:notin/@definitionURL"/>
  91   </xsl:variable>
  92   <xsl:variable name="charlength">
  93    <xsl:apply-templates select="m:notin" mode="charcount"/>
  94   </xsl:variable>
  95   <xsl:choose>
  96     <xsl:when test="$charlength > $framewidth">
  97      <xsl:text>(</xsl:text>
  98      <xsl:apply-templates select="*[2]">
  99       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 100      </xsl:apply-templates>
 101      <BR/>
 102      <xsl:call-template name="make_indent">
 103       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 104      </xsl:call-template>
 105      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
 106      <xsl:apply-templates select="*[3]">
 107       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 108      </xsl:apply-templates>
 109      <xsl:text>)</xsl:text>
 110     </xsl:when>
 111     <xsl:otherwise>
 112      <xsl:text>(</xsl:text>
 113      <xsl:apply-templates select="*[2]"/>
 114      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
 115      <xsl:apply-templates select="*[3]"/>
 116      <xsl:text>)</xsl:text>
 117     </xsl:otherwise>
 118    </xsl:choose>
 119  </xsl:template>
 120
 121 <!-- SET -->
 122
 123  <xsl:template match="m:set">
 124   <xsl:param name="current_indent" select="0"/>
 125   <xsl:param name="width" select="$framewidth"/>
 126   <xsl:variable name="uri">
 127    <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
 128   </xsl:variable>
 129   <xsl:choose>
 130    <xsl:when test="count(child::*) = 0">
 131     <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
 132    </xsl:when>
 133    <xsl:otherwise>
 134     <xsl:variable name="charlength">
 135      <xsl:apply-templates select="." mode="charcount"/>
 136     </xsl:variable>
 137     <xsl:choose>
 138      <xsl:when test="name(*[1]) = 'm:bvar'">
 139       <xsl:choose>
 140        <xsl:when test="$charlength > $framewidth">
 141         <xsl:text>{</xsl:text>
 142         <xsl:apply-templates select="m:bvar/m:ci"/>
 143         <xsl:text>:</xsl:text>
 144         <xsl:apply-templates select="m:bvar/m:type">
 145          <xsl:with-param name="current_indent"
 146            select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
 147         </xsl:apply-templates><BR/>
 148         <xsl:call-template name="make_indent">
 149          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 150         </xsl:call-template>
 151         <xsl:text>|</xsl:text>
 152         <xsl:apply-templates select="m:condition">
 153          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 154         </xsl:apply-templates>
 155         <xsl:text>}</xsl:text>
 156        </xsl:when>
 157        <xsl:otherwise>
 158         <xsl:text>{</xsl:text>
 159         <xsl:apply-templates select="m:bvar/m:ci"/>
 160         <xsl:text>:</xsl:text>
 161         <xsl:apply-templates select="m:bvar/m:type"/>
 162         <xsl:text>|</xsl:text>
 163         <xsl:apply-templates select="*[position()=2]"/>
 164         <xsl:text>}</xsl:text>
 165        </xsl:otherwise>
 166       </xsl:choose>
 167      </xsl:when>
 168      <xsl:otherwise>
 169       <xsl:choose>
 170        <xsl:when test="$charlength > $framewidth">
 171         <xsl:text>{</xsl:text>
 172          <xsl:apply-templates select="*[position()=1]">
 173           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 174          </xsl:apply-templates>
 175          <xsl:for-each select="*[position()>1]">
 176           <xsl:text>,</xsl:text>
 177           <BR/>
 178           <xsl:call-template name="make_indent">
 179            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 180           </xsl:call-template>
 181           <xsl:apply-templates select=".">
 182            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 183           </xsl:apply-templates>
 184          </xsl:for-each>
 185          <xsl:text>}</xsl:text>
 186         </xsl:when>
 187         <xsl:otherwise>
 188         <xsl:text>{</xsl:text>
 189          <xsl:for-each select="*">
 190           <xsl:apply-templates select="."/>
 191           <xsl:choose>
 192            <xsl:when test="position() = last()">
 193             <xsl:text>}</xsl:text>
 194            </xsl:when>
 195            <xsl:otherwise>
 196             <xsl:text>,</xsl:text>
 197            </xsl:otherwise>
 198           </xsl:choose>
 199          </xsl:for-each>
 200         </xsl:otherwise>
 201        </xsl:choose>
 202       </xsl:otherwise>
 203      </xsl:choose>
 204     </xsl:otherwise>
 205    </xsl:choose>
 206  </xsl:template>
 207
 208
 209 <!-- INTERSECTION -->
 210
 211 <xsl:template match="m:apply[m:intersect]">
 212   <xsl:param name="current_indent" select="0"/>
 213   <xsl:param name="width" select="$framewidth"/>
 214   <xsl:variable name="uri">
 215    <xsl:value-of select="m:intersect/@definitionURL"/>
 216   </xsl:variable>
 217   <xsl:variable name="charlength">
 218    <xsl:apply-templates select="m:intersect" mode="charcount"/>
 219   </xsl:variable>
 220   <xsl:choose>
 221     <xsl:when test="$charlength > $framewidth">
 222      <xsl:text>(</xsl:text>
 223      <xsl:apply-templates select="*[2]">
 224       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 225      </xsl:apply-templates>
 226      <BR/>
 227      <xsl:call-template name="make_indent">
 228       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 229      </xsl:call-template>
 230      <a>
 231      <xsl:attribute name="href">
 232       <xsl:value-of select="concat(string($header),string($uri))"/>
 233      </xsl:attribute>
 234      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
 235      </a>
 236      <xsl:apply-templates select="*[3]">
 237       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 238      </xsl:apply-templates>
 239      <xsl:text>)</xsl:text>
 240     </xsl:when>
 241     <xsl:otherwise>
 242      <xsl:text>(</xsl:text>
 243      <xsl:apply-templates select="*[2]"/>
 244      <a>
 245      <xsl:attribute name="href">
 246       <xsl:value-of select="concat(string($header),string($uri))"/>
 247      </xsl:attribute>
 248      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
 249      </a>
 250      <xsl:apply-templates select="*[3]"/>
 251      <xsl:text>)</xsl:text>
 252     </xsl:otherwise>
 253    </xsl:choose>
 254  </xsl:template>
 255
 256 <!-- UNION -->
 257
 258 <xsl:template match="m:apply[m:union]">
 259   <xsl:param name="current_indent" select="0"/>
 260   <xsl:param name="width" select="$framewidth"/>
 261   <xsl:variable name="uri">
 262    <xsl:value-of select="m:union/@definitionURL"/>
 263   </xsl:variable>
 264   <xsl:variable name="charlength">
 265    <xsl:apply-templates select="m:union" mode="charcount"/>
 266   </xsl:variable>
 267   <xsl:choose>
 268     <xsl:when test="$charlength > $framewidth">
 269      <xsl:text>(</xsl:text>
 270      <xsl:apply-templates select="*[2]">
 271       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 272      </xsl:apply-templates>
 273      <BR/>
 274      <xsl:call-template name="make_indent">
 275       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 276      </xsl:call-template>
 277      <a>
 278      <xsl:attribute name="href">
 279       <xsl:value-of select="concat(string($header),string($uri))"/>
 280      </xsl:attribute>
 281      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
 282      </a>
 283      <xsl:apply-templates select="*[3]">
 284       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 285      </xsl:apply-templates>
 286      <xsl:text>)</xsl:text>
 287     </xsl:when>
 288     <xsl:otherwise>
 289      <xsl:text>(</xsl:text>
 290      <xsl:apply-templates select="*[2]"/>
 291      <a>
 292      <xsl:attribute name="href">
 293       <xsl:value-of select="concat(string($header),string($uri))"/>
 294      </xsl:attribute>
 295      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
 296      </a>
 297      <xsl:apply-templates select="*[3]"/>
 298      <xsl:text>)</xsl:text>
 299     </xsl:otherwise>
 300    </xsl:choose>
 301  </xsl:template>
 302
 303 <!-- SUBSET -->
 304 <xsl:template match="m:apply[m:subset]">
 305   <xsl:param name="current_indent" select="0"/>
 306   <xsl:param name="width" select="$framewidth"/>
 307   <xsl:variable name="uri">
 308    <xsl:value-of select="m:subset/@definitionURL"/>
 309   </xsl:variable>
 310   <xsl:variable name="charlength">
 311    <xsl:apply-templates select="m:subset" mode="charcount"/>
 312   </xsl:variable>
 313   <xsl:choose>
 314     <xsl:when test="$charlength > $framewidth">
 315      <xsl:text>(</xsl:text>
 316      <xsl:apply-templates select="*[2]">
 317       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 318      </xsl:apply-templates>
 319      <BR/>
 320      <xsl:call-template name="make_indent">
 321       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 322      </xsl:call-template>
 323      <a>
 324      <xsl:attribute name="href">
 325       <xsl:value-of select="concat(string($header),string($uri))"/>
 326      </xsl:attribute>
 327      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
 328      </a>
 329      <xsl:apply-templates select="*[3]">
 330       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 331      </xsl:apply-templates>
 332      <xsl:text>)</xsl:text>
 333     </xsl:when>
 334     <xsl:otherwise>
 335      <xsl:text>(</xsl:text>
 336      <xsl:apply-templates select="*[2]"/>
 337      <a>
 338      <xsl:attribute name="href">
 339       <xsl:value-of select="concat(string($header),string($uri))"/>
 340      </xsl:attribute>
 341      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
 342      </a>
 343      <xsl:apply-templates select="*[3]"/>
 344      <xsl:text>)</xsl:text>
 345     </xsl:otherwise>
 346    </xsl:choose>
 347  </xsl:template>
 348
 349 <!-- PRSUBSET -->
 350 <xsl:template match="m:apply[m:prsubset]">
 351   <xsl:param name="current_indent" select="0"/>
 352   <xsl:param name="width" select="$framewidth"/>
 353   <xsl:variable name="uri">
 354    <xsl:value-of select="m:prsubset/@definitionURL"/>
 355   </xsl:variable>
 356   <xsl:variable name="charlength">
 357    <xsl:apply-templates select="m:prsubset" mode="charcount"/>
 358   </xsl:variable>
 359   <xsl:choose>
 360     <xsl:when test="$charlength > $framewidth">
 361      <xsl:text>(</xsl:text>
 362      <xsl:apply-templates select="*[2]">
 363       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 364      </xsl:apply-templates>
 365      <BR/>
 366      <xsl:call-template name="make_indent">
 367       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 368      </xsl:call-template>
 369      <a>
 370      <xsl:attribute name="href">
 371       <xsl:value-of select="concat(string($header),string($uri))"/>
 372      </xsl:attribute>
 373      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
 374      </a>
 375      <xsl:apply-templates select="*[3]">
 376       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 377      </xsl:apply-templates>
 378      <xsl:text>)</xsl:text>
 379     </xsl:when>
 380     <xsl:otherwise>
 381      <xsl:text>(</xsl:text>
 382      <xsl:apply-templates select="*[2]"/>
 383      <a>
 384      <xsl:attribute name="href">
 385       <xsl:value-of select="concat(string($header),string($uri))"/>
 386      </xsl:attribute>
 387      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
 388      </a>
 389      <xsl:apply-templates select="*[3]"/>
 390      <xsl:text>)</xsl:text>
 391     </xsl:otherwise>
 392    </xsl:choose>
 393  </xsl:template>
 394
 395
 396 <!-- SETDIFF -->
 397
 398 <xsl:template match="m:apply[m:setdiff]">
 399   <xsl:param name="current_indent" select="0"/>
 400   <xsl:param name="width" select="$framewidth"/>
 401   <xsl:variable name="uri">
 402    <xsl:value-of select="m:setdiff/@definitionURL"/>
 403   </xsl:variable>
 404   <xsl:variable name="charlength">
 405    <xsl:apply-templates select="m:setdiff" mode="charcount"/>
 406   </xsl:variable>
 407   <xsl:choose>
 408     <xsl:when test="$charlength > $framewidth">
 409      <xsl:text>(</xsl:text>
 410      <xsl:apply-templates select="*[2]">
 411       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 412      </xsl:apply-templates>
 413      <BR/>
 414      <xsl:call-template name="make_indent">
 415       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 416      </xsl:call-template>
 417      <a>
 418      <xsl:attribute name="href">
 419       <xsl:value-of select="concat(string($header),string($uri))"/>
 420      </xsl:attribute>
 421      <xsl:text>/</xsl:text>
 422      </a>
 423      <xsl:apply-templates select="*[3]">
 424       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 425      </xsl:apply-templates>
 426      <xsl:text>)</xsl:text>
 427     </xsl:when>
 428     <xsl:otherwise>
 429      <xsl:text>(</xsl:text>
 430      <xsl:apply-templates select="*[2]"/>
 431      <a>
 432      <xsl:attribute name="href">
 433       <xsl:value-of select="concat(string($header),string($uri))"/>
 434      </xsl:attribute>
 435      <xsl:text>/</xsl:text>
 436      </a>
 437      <xsl:apply-templates select="*[3]"/>
 438      <xsl:text>)</xsl:text>
 439     </xsl:otherwise>
 440    </xsl:choose>
 441  </xsl:template>
 442
 443 <!-- CARD -->
 444 <xsl:template match="m:apply[m:card]">
 445   <xsl:param name="current_indent" select="0"/>
 446   <xsl:param name="width" select="$framewidth"/>
 447   <xsl:variable name="uri">
 448    <xsl:value-of select="m:card/@definitionURL"/>
 449   </xsl:variable>
 450   <xsl:text>|</xsl:text>
 451   <xsl:apply-templates select="*[2]">
 452    <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 453   </xsl:apply-templates>
 454   <xsl:text>|</xsl:text>
 455  </xsl:template>
 456
 457 <!-- COUNTING -->
 458
 459 <xsl:template match="m:in|m:notin|m:intersect|m:union
 460            |m:subset|m:prsubset|m:setdiff|m:card" mode="charcount">
 461 <xsl:param name="incurrent_length" select="0"/>
 462     <xsl:choose>
 463     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 464      <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>
 465      <xsl:choose>
 466      <xsl:when test="string($siblength) = &quot;&quot;">
 467       <xsl:value-of select="$incurrent_length + string-length()"/>
 468      </xsl:when>
 469      <xsl:otherwise>
 470       <xsl:value-of select="number($siblength)"/>
 471      </xsl:otherwise>
 472      </xsl:choose>
 473     </xsl:when>
 474     <xsl:otherwise>
 475      <xsl:value-of select="$incurrent_length + string-length()"/>
 476     </xsl:otherwise>
 477     </xsl:choose>
 478 </xsl:template>
 479
 480 </xsl:stylesheet>
 481
 482
 483
 484
 485
 486
 487