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:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
 169        |m:geq|m:gt|m:plus|m:times|m:divide]">
 170   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 171   <xsl:text>(</xsl:text>
 172   <xsl:apply-templates mode="inline" select="*[2]"/>
 173   <xsl:choose>
 174   <xsl:when test="$uri != ''">
 175    <a href="{$uri}">
 176     <xsl:call-template name="mksymbol-init">
 177      <xsl:with-param name="symbol" select="local-name(*[1])"/>
 178     </xsl:call-template>
 179    </a>
 180   </xsl:when>
 181   <xsl:otherwise>
 182    <xsl:call-template name="mksymbol-init">
 183      <xsl:with-param name="symbol" select="local-name(*[1])"/>
 184    </xsl:call-template>
 185   </xsl:otherwise>
 186   </xsl:choose>
 187   <xsl:apply-templates mode="inline" select="*[3]"/>
 188   <xsl:text>)</xsl:text>
 189  </xsl:template>
 190
 191 <!-- INLINE MODE - MINUS (can be unary!) -->
 192
 193 <xsl:template mode="inline" match="m:apply[m:minus]">
 194   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 195   <xsl:choose>
 196    <xsl:when test="count(child::*)=2">
 197     <xsl:choose>
 198     <xsl:when test="$uri != ''">
 199      <a href="{$uri}">
 200       <xsl:call-template name="mksymbol-init">
 201        <xsl:with-param name="symbol" select="'minus'"/>
 202       </xsl:call-template>
 203      </a>
 204     </xsl:when>
 205     <xsl:otherwise>
 206      <xsl:call-template name="mksymbol-init">
 207        <xsl:with-param name="symbol" select="'minus'"/>
 208      </xsl:call-template>
 209     </xsl:otherwise>
 210     </xsl:choose>
 211     <xsl:apply-templates mode="inline" select="*[2]"/>
 212    </xsl:when>
 213    <xsl:otherwise>
 214     <xsl:text>(</xsl:text>
 215     <xsl:apply-templates mode="inline" select="*[2]"/>
 216     <xsl:choose>
 217     <xsl:when test="$uri != ''">
 218      <a href="{$uri}">
 219       <xsl:call-template name="mksymbol-init">
 220        <xsl:with-param name="symbol" select="'minus'"/>
 221       </xsl:call-template>
 222      </a>
 223     </xsl:when>
 224     <xsl:otherwise>
 225      <xsl:call-template name="mksymbol-init">
 226        <xsl:with-param name="symbol" select="'minus'"/>
 227      </xsl:call-template>
 228     </xsl:otherwise>
 229     </xsl:choose>
 230     <xsl:apply-templates mode="inline" select="*[3]"/>
 231     <xsl:text>)</xsl:text>
 232    </xsl:otherwise>
 233   </xsl:choose>
 234  </xsl:template>
 235
 236 <!-- INLINE MODE NOT -->
 237
 238 <xsl:template mode="inline" match="m:apply[m:not]">
 239   <xsl:variable name="uri"><xsl:value-of select="m:not/@definitionURL"/></xsl:variable>
 240   <xsl:choose>
 241   <xsl:when test="$uri != ''">
 242    <a href="{$uri}">
 243     <xsl:call-template name="mksymbol-init">
 244      <xsl:with-param name="symbol" select="'not'"/>
 245     </xsl:call-template>
 246    </a>
 247   </xsl:when>
 248   <xsl:otherwise>
 249    <xsl:call-template name="mksymbol-init">
 250     <xsl:with-param name="symbol" select="'not'"/>
 251    </xsl:call-template>
 252   </xsl:otherwise>
 253   </xsl:choose>
 254   <xsl:apply-templates mode="inline" select="*[2]"/>
 255 </xsl:template>
 256
 257 <!-- INLINE MODE EXISTS -->
 258
 259  <xsl:template mode="inline" match="m:apply[m:exists]">
 260   <xsl:variable name="uri"><xsl:value-of select="m:exists/@definitionURL"/></xsl:variable>
 261   <xsl:choose>
 262   <xsl:when test="$uri != ''">
 263    <a href="{$uri}">
 264     <xsl:call-template name="mksymbol-init">
 265      <xsl:with-param name="symbol" select="'exists'"/>
 266     </xsl:call-template>
 267    </a>
 268   </xsl:when>
 269   <xsl:otherwise>
 270    <xsl:call-template name="mksymbol-init">
 271     <xsl:with-param name="symbol" select="'exists'"/>
 272    </xsl:call-template>
 273   </xsl:otherwise>
 274   </xsl:choose>
 275   <xsl:apply-templates select="m:bvar/m:ci"/>
 276   <xsl:text>:</xsl:text>
 277   <xsl:apply-templates mode="inline" select="m:condition"/>
 278   <xsl:text>.</xsl:text>
 279   <xsl:apply-templates mode="inline" select="*[last()]"/>
 280  </xsl:template>
 281
 282 <!-- COUNTING MODE -->
 283
 284 <!-- BASIC OPERATORS -->
 285
 286  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
 287        |m:geq|m:gt|m:plus|m:times|m:divide]">
 288   <xsl:param name="current_indent" select="0"/>
 289   <xsl:param name="width" select="$framewidth"/>
 290   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 291   <xsl:variable name="charlength">
 292    <xsl:apply-templates select="*[1]" mode="charcount"/>
 293   </xsl:variable>
 294   <xsl:choose>
 295     <xsl:when test="$charlength > $framewidth">
 296      <xsl:text>(</xsl:text>
 297      <xsl:apply-templates select="*[2]">
 298       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 299      </xsl:apply-templates>
 300      <BR/>
 301      <xsl:call-template name="make_indent">
 302       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 303      </xsl:call-template>
 304      <xsl:choose>
 305      <xsl:when test="$uri != ''">
 306       <a href="{$uri}">
 307        <xsl:call-template name="mksymbol-init">
 308         <xsl:with-param name="symbol" select="local-name(*[1])"/>
 309        </xsl:call-template>
 310       </a>
 311      </xsl:when>
 312      <xsl:otherwise>
 313        <xsl:call-template name="mksymbol-init">
 314         <xsl:with-param name="symbol" select="local-name(*[1])"/>
 315        </xsl:call-template>
 316      </xsl:otherwise>
 317      </xsl:choose>
 318      <xsl:apply-templates select="*[3]">
 319       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 320      </xsl:apply-templates>
 321      <xsl:text>)</xsl:text>
 322     </xsl:when>
 323     <xsl:otherwise>
 324      <xsl:apply-templates mode="inline" select="."/>
 325     </xsl:otherwise>
 326    </xsl:choose>
 327  </xsl:template>
 328
 329 <!-- MINUS (can be unary!) -->
 330
 331 <xsl:template match="m:apply[m:minus]">
 332   <xsl:param name="current_indent" select="0"/>
 333   <xsl:param name="width" select="$framewidth"/>
 334   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 335   <xsl:choose>
 336    <xsl:when test="count(child::*)=2">
 337     <xsl:choose>
 338     <xsl:when test="$uri != ''">
 339      <a href="{$uri}">
 340       <xsl:call-template name="mksymbol-init">
 341        <xsl:with-param name="symbol" select="'minus'"/>
 342       </xsl:call-template>
 343      </a>
 344     </xsl:when>
 345     <xsl:otherwise>
 346       <xsl:call-template name="mksymbol-init">
 347        <xsl:with-param name="symbol" select="'minus'"/>
 348       </xsl:call-template>
 349     </xsl:otherwise>
 350     </xsl:choose>
 351     <xsl:apply-templates select="*[2]">
 352      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
 353     </xsl:apply-templates>
 354    </xsl:when>
 355    <xsl:otherwise>
 356     <xsl:variable name="charlength">
 357      <xsl:apply-templates select="*[1]" 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       <xsl:choose>
 370       <xsl:when test="$uri != ''">
 371        <a href="{$uri}">
 372         <xsl:call-template name="mksymbol-init">
 373          <xsl:with-param name="symbol" select="'minus'"/>
 374         </xsl:call-template>
 375        </a>
 376       </xsl:when>
 377       <xsl:otherwise>
 378         <xsl:call-template name="mksymbol-init">
 379          <xsl:with-param name="symbol" select="'minus'"/>
 380         </xsl:call-template>
 381       </xsl:otherwise>
 382       </xsl:choose>
 383       <xsl:apply-templates select="*[3]">
 384        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 385       </xsl:apply-templates>
 386       <xsl:text>)</xsl:text>
 387      </xsl:when>
 388      <xsl:otherwise>
 389       <xsl:apply-templates mode="inline" select="."/>
 390      </xsl:otherwise>
 391     </xsl:choose>
 392    </xsl:otherwise>
 393   </xsl:choose>
 394  </xsl:template>
 395
 396 <!-- NOT -->
 397
 398 <xsl:template match="m:apply[m:not]">
 399   <xsl:param name="current_indent" select="0"/>
 400   <xsl:param name="width" select="$framewidth"/>
 401   <xsl:variable name="uri"><xsl:value-of select="m:not/@definitionURL"/></xsl:variable>
 402    <xsl:choose>
 403    <xsl:when test="$uri != ''">
 404     <a href="{$uri}">
 405      <xsl:call-template name="mksymbol-init">
 406       <xsl:with-param name="symbol" select="'not'"/>
 407      </xsl:call-template>
 408     </a>
 409    </xsl:when>
 410    <xsl:otherwise>
 411      <xsl:call-template name="mksymbol-init">
 412       <xsl:with-param name="symbol" select="'not'"/>
 413      </xsl:call-template>
 414    </xsl:otherwise>
 415    </xsl:choose>
 416    <xsl:apply-templates select="*[2]"/>
 417  </xsl:template>
 418
 419 <!-- EXISTS -->
 420
 421  <xsl:template match="m:apply[m:exists]">
 422   <xsl:param name="current_indent" select="0"/>
 423   <xsl:param name="width" select="$framewidth"/>
 424   <xsl:variable name="uri"><xsl:value-of select="m:exists/@definitionURL"/></xsl:variable>
 425   <xsl:variable name="charlength">
 426    <xsl:apply-templates select="m:exists" mode="charcount"/>
 427   </xsl:variable>
 428   <xsl:choose>
 429     <xsl:when test="$charlength > $framewidth">
 430      <xsl:choose>
 431      <xsl:when test="$uri != ''">
 432       <a href="{$uri}">
 433        <xsl:call-template name="mksymbol-init">
 434         <xsl:with-param name="symbol" select="'exists'"/>
 435        </xsl:call-template>
 436       </a>
 437      </xsl:when>
 438      <xsl:otherwise>
 439        <xsl:call-template name="mksymbol-init">
 440         <xsl:with-param name="symbol" select="'exists'"/>
 441        </xsl:call-template>
 442      </xsl:otherwise>
 443      </xsl:choose>
 444      <xsl:apply-templates select="m:bvar/m:ci"/>
 445      <xsl:text>:</xsl:text>
 446      <xsl:apply-templates select="m:condition">
 447       <xsl:with-param name="current_indent" select="$current_indent + 2 +
 448                                 string-length(bvar/ci)"/>
 449      </xsl:apply-templates>
 450      <BR/>
 451       <xsl:call-template name="make_indent">
 452        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 453       </xsl:call-template>
 454      <xsl:text>.</xsl:text>
 455       <xsl:apply-templates select="*[last()]">
 456        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 457       </xsl:apply-templates>
 458     </xsl:when>
 459     <xsl:otherwise>
 460      <xsl:apply-templates mode="inline" select="."/>
 461     </xsl:otherwise>
 462    </xsl:choose>
 463  </xsl:template>
 464
 465
 466
 467
 468 <!-- COUNTING -->
 469
 470 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
 471    |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
 472 <xsl:param name="incurrent_length" select="0"/>
 473     <xsl:choose>
 474     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 475      <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>
 476      <xsl:choose>
 477      <xsl:when test="string($siblength) = &quot;&quot;">
 478       <xsl:value-of select="$incurrent_length + string-length()"/>
 479      </xsl:when>
 480      <xsl:otherwise>
 481       <xsl:value-of select="number($siblength)"/>
 482      </xsl:otherwise>
 483      </xsl:choose>
 484     </xsl:when>
 485     <xsl:otherwise>
 486      <xsl:value-of select="$incurrent_length + string-length()"/>
 487     </xsl:otherwise>
 488     </xsl:choose>
 489 </xsl:template>
 490
 491 </xsl:stylesheet>