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">
 149    <xsl:value-of select="*[1]/@definitionURL"/>
 150   </xsl:variable>
 151   <xsl:text>(</xsl:text>
 152   <xsl:apply-templates mode="inline" select="*[2]"/>
 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:apply-templates mode="inline" select="*[3]"/>
 159   <xsl:text>)</xsl:text>
 160  </xsl:template>
 161
 162 <!-- INLINE MODE - MINUS (can be unary!) -->
 163
 164 <xsl:template mode="inline" match="m:apply[m:minus]">
 165   <xsl:variable name="uri">
 166    <xsl:value-of select="*[1]/@definitionURL"/>
 167   </xsl:variable>
 168   <xsl:choose>
 169    <xsl:when test="count(child::*)=2">
 170     <a href="{$uri}">
 171      <xsl:call-template name="mksymbol-init">
 172       <xsl:with-param name="symbol" select="'minus'"/>
 173      </xsl:call-template>
 174     </a>
 175     <xsl:apply-templates mode="inline" select="*[2]"/>
 176    </xsl:when>
 177    <xsl:otherwise>
 178     <xsl:text>(</xsl:text>
 179     <xsl:apply-templates mode="inline" select="*[2]"/>
 180     <a href="{$uri}">
 181      <xsl:call-template name="mksymbol-init">
 182       <xsl:with-param name="symbol" select="'minus'"/>
 183      </xsl:call-template>
 184     </a>
 185     <xsl:apply-templates mode="inline" select="*[3]"/>
 186     <xsl:text>)</xsl:text>
 187    </xsl:otherwise>
 188   </xsl:choose>
 189  </xsl:template>
 190
 191 <!-- INLINE MODE NOT -->
 192
 193  <xsl:template mode="inline" match="m:apply[m:not]">
 194   <xsl:variable name="uri">
 195    <xsl:value-of select="m:not/@definitionURL"/>
 196   </xsl:variable>
 197      <a href="{$uri}">
 198       <xsl:call-template name="mksymbol-init">
 199        <xsl:with-param name="symbol" select="'not'"/>
 200       </xsl:call-template>
 201      </a>
 202      <xsl:apply-templates mode="inline" select="*[2]"/>
 203  </xsl:template>
 204
 205 <!-- INLINE MODE EXISTS -->
 206
 207  <xsl:template mode="inline" match="m:apply[m:exists]">
 208   <xsl:variable name="uri">
 209    <xsl:value-of select="m:exists/@definitionURL"/>
 210   </xsl:variable>
 211   <a href="{$uri}">
 212    <xsl:call-template name="mksymbol-init">
 213     <xsl:with-param name="symbol" select="'exists'"/>
 214    </xsl:call-template>
 215   </a>
 216   <xsl:apply-templates select="m:bvar/m:ci"/>
 217   <xsl:text>:</xsl:text>
 218   <xsl:apply-templates mode="inline" select="m:condition"/>
 219   <xsl:text>.</xsl:text>
 220   <xsl:apply-templates mode="inline" select="*[last()]"/>
 221  </xsl:template>
 222
 223 <!-- COUNTING MODE -->
 224
 225 <!-- BASIC OPERATORS -->
 226
 227  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
 228        |m:geq|m:gt|m:plus|m:times]">
 229   <xsl:param name="current_indent" select="0"/>
 230   <xsl:param name="width" select="$framewidth"/>
 231   <xsl:variable name="uri">
 232    <xsl:value-of select="*[1]/@definitionURL"/>
 233   </xsl:variable>
 234   <xsl:variable name="charlength">
 235    <xsl:apply-templates select="*[1]" mode="charcount"/>
 236   </xsl:variable>
 237   <xsl:choose>
 238     <xsl:when test="$charlength > $framewidth">
 239      <xsl:text>(</xsl:text>
 240      <xsl:apply-templates select="*[2]">
 241       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 242      </xsl:apply-templates>
 243      <BR/>
 244      <xsl:call-template name="make_indent">
 245       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 246      </xsl:call-template>
 247      <a href="{$uri}">
 248       <xsl:call-template name="mksymbol-init">
 249        <xsl:with-param name="symbol" select="local-name(*[1])"/>
 250       </xsl:call-template>
 251      </a>
 252      <xsl:apply-templates select="*[3]">
 253       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 254      </xsl:apply-templates>
 255      <xsl:text>)</xsl:text>
 256     </xsl:when>
 257     <xsl:otherwise>
 258      <xsl:apply-templates mode="inline" select="."/>
 259     </xsl:otherwise>
 260    </xsl:choose>
 261  </xsl:template>
 262
 263 <!-- MINUS (can be unary!) -->
 264
 265 <xsl:template match="m:apply[m:minus]">
 266   <xsl:param name="current_indent" select="0"/>
 267   <xsl:param name="width" select="$framewidth"/>
 268   <xsl:variable name="uri">
 269    <xsl:value-of select="*[1]/@definitionURL"/>
 270   </xsl:variable>
 271   <xsl:choose>
 272    <xsl:when test="count(child::*)=2">
 273     <a href="{$uri}">
 274      <xsl:call-template name="mksymbol-init">
 275       <xsl:with-param name="symbol" select="'minus'"/>
 276      </xsl:call-template>
 277     </a>
 278     <xsl:apply-templates select="*[2]">
 279      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
 280     </xsl:apply-templates>
 281    </xsl:when>
 282    <xsl:otherwise>
 283     <xsl:variable name="charlength">
 284      <xsl:apply-templates select="*[1]" mode="charcount"/>
 285     </xsl:variable>
 286     <xsl:choose>
 287      <xsl:when test="$charlength > $framewidth">
 288       <xsl:text>(</xsl:text>
 289       <xsl:apply-templates select="*[2]">
 290        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 291       </xsl:apply-templates>
 292       <BR/>
 293       <xsl:call-template name="make_indent">
 294        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 295       </xsl:call-template>
 296       <a href="{$uri}">
 297        <xsl:call-template name="mksymbol-init">
 298         <xsl:with-param name="symbol" select="'minus'"/>
 299        </xsl:call-template>
 300       </a>
 301       <xsl:apply-templates select="*[3]">
 302        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 303       </xsl:apply-templates>
 304       <xsl:text>)</xsl:text>
 305      </xsl:when>
 306      <xsl:otherwise>
 307       <xsl:apply-templates mode="inline" select="."/>
 308      </xsl:otherwise>
 309     </xsl:choose>
 310    </xsl:otherwise>
 311   </xsl:choose>
 312  </xsl:template>
 313
 314 <!-- NOT -->
 315
 316  <xsl:template match="m:apply[m:not]">
 317   <xsl:param name="current_indent" select="0"/>
 318   <xsl:param name="width" select="$framewidth"/>
 319   <xsl:variable name="uri">
 320    <xsl:value-of select="m:not/@definitionURL"/>
 321   </xsl:variable>
 322      <a href="{$uri}">
 323       <xsl:call-template name="mksymbol-init">
 324        <xsl:with-param name="symbol" select="'not'"/>
 325       </xsl:call-template>
 326      </a>
 327      <xsl:apply-templates select="*[2]"/>
 328  </xsl:template>
 329
 330 <!-- EXISTS -->
 331
 332  <xsl:template match="m:apply[m:exists]">
 333   <xsl:param name="current_indent" select="0"/>
 334   <xsl:param name="width" select="$framewidth"/>
 335   <xsl:variable name="uri">
 336    <xsl:value-of select="m:exists/@definitionURL"/>
 337   </xsl:variable>
 338   <xsl:variable name="charlength">
 339    <xsl:apply-templates select="m:exists" mode="charcount"/>
 340   </xsl:variable>
 341   <xsl:choose>
 342     <xsl:when test="$charlength > $framewidth">
 343      <a href="{$uri}">
 344       <xsl:call-template name="mksymbol-init">
 345        <xsl:with-param name="symbol" select="'exists'"/>
 346       </xsl:call-template>
 347      </a>
 348      <xsl:apply-templates select="m:bvar/m:ci"/>
 349      <xsl:text>:</xsl:text>
 350      <xsl:apply-templates select="m:condition">
 351       <xsl:with-param name="current_indent" select="$current_indent + 2 +
 352                                 string-length(bvar/ci)"/>
 353      </xsl:apply-templates>
 354      <BR/>
 355       <xsl:call-template name="make_indent">
 356        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 357       </xsl:call-template>
 358      <xsl:text>.</xsl:text>
 359       <xsl:apply-templates select="*[last()]">
 360        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 361       </xsl:apply-templates>
 362     </xsl:when>
 363     <xsl:otherwise>
 364      <xsl:apply-templates mode="inline" select="."/>
 365     </xsl:otherwise>
 366    </xsl:choose>
 367  </xsl:template>
 368
 369
 370
 371
 372 <!-- COUNTING -->
 373
 374 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
 375    |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
 376 <xsl:param name="incurrent_length" select="0"/>
 377     <xsl:choose>
 378     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
 379      <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>
 380      <xsl:choose>
 381      <xsl:when test="string($siblength) = &quot;&quot;">
 382       <xsl:value-of select="$incurrent_length + string-length()"/>
 383      </xsl:when>
 384      <xsl:otherwise>
 385       <xsl:value-of select="number($siblength)"/>
 386      </xsl:otherwise>
 387      </xsl:choose>
 388     </xsl:when>
 389     <xsl:otherwise>
 390      <xsl:value-of select="$incurrent_length + string-length()"/>
 391     </xsl:otherwise>
 392     </xsl:choose>
 393 </xsl:template>
 394
 395 </xsl:stylesheet>
 396
 397