UNICODEvsSYMBOL introduced

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index b070e87fcfb03420ce8129c7380c96f32073c2cf..85498997fd6bd1bcb0b4b56595d7083feb9a2f4a 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -81,6 +81,30 @@
       <xsl:when test="$symbol = 'arrow'">
        <xsl:value-of select="'&#x00ae;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'RightArrow'">
+       <xsl:value-of select="'&#222;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'subst'">
+       <xsl:value-of select="'&#x00ac;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+       <xsl:value-of select="'&#x00ad;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+       <xsl:value-of select="'&#x00ae;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta'">
+       <xsl:value-of select="'&#x0062;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+       <xsl:value-of select="'&#x00de;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'isomorphic'">
+       <xsl:value-of select="'&#x0040;'"/>
+      </xsl:when>
+      <xsl:otherwise>
+       <xsl:text>???</xsl:text>
+      </xsl:otherwise>
      </xsl:choose>
     </xsl:variable>
     <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
@@ -102,6 +126,30 @@
       <xsl:when test="$symbol = 'arrow'">
        <xsl:value-of select="'&#8594;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'RightArrow'">
+       <xsl:value-of select="'&#8658;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'subst'">
+       <xsl:value-of select="'&#8592;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+       <xsl:value-of select="'&#8593;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+       <xsl:value-of select="'&#8594;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta'">
+       <xsl:value-of select="'&#946;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+       <xsl:value-of select="'&#8658;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'isomorphic'">
+       <xsl:value-of select="'&#8773;'"/>
+      </xsl:when>
+      <xsl:otherwise>
+       <xsl:text>???</xsl:text>
+      </xsl:otherwise>
      </xsl:choose>
     </xsl:variable>
     <FONT color="{$color}">
@@ -280,7 +328,11 @@
        </xsl:when> 
       </xsl:choose>
       <xsl:apply-templates mode="inline" select="."/>
-      <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
+      <xsl:call-template name="mksymbol-1">
+       <xsl:with-param name="symbol" select="'RightArrow'"/>
+       <xsl:with-param name="color" select="'green'"/>
+       <xsl:with-param name="size" select="'+0'"/>
+      </xsl:call-template>
       <xsl:apply-templates mode="inline"
            select="following-sibling::*[position()= 1]"/>
      </xsl:for-each>
@@ -364,9 +416,11 @@
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ac;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <xsl:text>]</xsl:text>
@@ -377,9 +431,11 @@
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
@@ -391,9 +447,11 @@
 
       <xsl:when test="$name='lift'">
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
@@ -407,13 +465,17 @@
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -422,13 +484,18 @@
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -437,13 +504,17 @@
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -452,13 +523,18 @@
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -477,9 +553,11 @@
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-        <FONT color="green" FACE="symbol">
-        <xsl:text>&#x0040;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
@@ -701,7 +779,11 @@
             </xsl:otherwise>
             </xsl:choose>
             <xsl:apply-templates select="."/>
-            <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
+            <xsl:call-template name="mksymbol-1">
+             <xsl:with-param name="symbol" select="'RightArrow'"/>
+             <xsl:with-param name="color" select="'green'"/>
+             <xsl:with-param name="size" select="'+0'"/>
+            </xsl:call-template>
             <xsl:variable name="body_size">
              <xsl:apply-templates 
               select="following-sibling::*[1]/*[1]" mode="charcount"/>
@@ -1055,7 +1137,11 @@
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
        <xsl:text>0&#x00a0;</xsl:text>
-       <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
+       <xsl:call-template name="mksymbol-1">
+        <xsl:with-param name="symbol" select="'RightArrow'"/>
+        <xsl:with-param name="color" select="'green'"/>
+        <xsl:with-param name="size" select="'+0'"/>
+       </xsl:call-template>
        <xsl:apply-templates select="*[3]">
         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
        </xsl:apply-templates>
@@ -1066,7 +1152,11 @@
        <xsl:text>S(</xsl:text>
        <xsl:apply-templates select="*[4]"/>
        <xsl:text>)&#x00a0;</xsl:text>
-       <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
+       <xsl:call-template name="mksymbol-1">
+        <xsl:with-param name="symbol" select="'RightArrow'"/>
+        <xsl:with-param name="color" select="'green'"/>
+        <xsl:with-param name="size" select="'+0'"/>
+       </xsl:call-template>
        <FONT color="red">Assume by induction</FONT>
        <br/>
        <xsl:call-template name="make_indent">
@@ -1286,9 +1376,11 @@
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="blue" SIZE="+0" FACE="symbol">
-        <xsl:text>&#x00ac;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'blue'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[2]"/>
        <xsl:text>]</xsl:text>
@@ -1299,9 +1391,11 @@
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
@@ -1313,9 +1407,11 @@
 
       <xsl:when test="$name='lift'">
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
@@ -1329,13 +1425,17 @@
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1344,13 +1444,18 @@
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1359,13 +1464,17 @@
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1374,13 +1483,18 @@
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1399,9 +1513,11 @@
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-        <FONT color="green" FACE="symbol">
-        <xsl:text>&#x0040;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>