helm/style/html_set.xsl

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