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