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