UNICODEvsSYMBOL parameter added to select the old

[helm.git] / helm / style / content_to_html.xsl

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 5a48cc1ea49933cc3b3d492a119822d5c07f8353..4b51eb320c86729ac0d468e62836a916ac872db7 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -34,6 +34,7 @@
 
 <xsl:param name="CICURI" select="''"/>
 <xsl:param name="type" select="'standalone'"/>
+<xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
 
 <xsl:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
@@ -60,6 +61,56 @@
 
 <xsl:variable name="framewidth" select="45"/>
 
+<xsl:template name="mksymbol-1">
+ <xsl:param name="symbol" select="''"/>
+ <xsl:param name="color" select="''"/>
+ <xsl:param name="size" select="''"/>
+  <xsl:choose>
+   <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
+    <xsl:variable name="fontsymbol">
+     <xsl:choose>
+      <xsl:when test="$symbol = 'forall'">
+       <xsl:value-of select="'&#x22;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lambda'">
+       <xsl:value-of select="'l'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'prod'">
+       <xsl:value-of select="'&#x00d5;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'arrow'">
+       <xsl:value-of select="'&#x00ae;'"/>
+      </xsl:when>
+     </xsl:choose>
+    </xsl:variable>
+    <FONT FACE="symbol" SIZE="{$size}" mathcolor="{$color}">
+     <xsl:value-of select="$fontsymbol"/>
+    </FONT>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:variable name="unicodesymbol">
+     <xsl:choose>
+      <xsl:when test="$symbol = 'forall'">
+       <xsl:value-of select="'&#8704;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lambda'">
+       <xsl:value-of select="'&#955;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'prod'">
+       <xsl:value-of select="'&#928;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'arrow'">
+       <xsl:value-of select="'&#8594;'"/>
+      </xsl:when>
+     </xsl:choose>
+    </xsl:variable>
+    <FONT color="{$color}">
+     <xsl:value-of select="$unicodesymbol"/>
+    </FONT>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
 <xsl:template match="/">
  <xsl:param name="current_indent" select="0"/>
  <xsl:choose>
@@ -152,7 +203,11 @@
    <xsl:choose>
     <!-- FORALL -->
     <xsl:when test="$name='forall'">
-     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</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="'+2'"/>
+     </xsl:call-template>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
@@ -160,7 +215,11 @@
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
     </xsl:when>
     <xsl:when test="$name='prod'">
-     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</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="'+2'"/>
+     </xsl:call-template>
      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
@@ -171,9 +230,11 @@
     <xsl:when test="$name='arrow'">
      <xsl:text>(</xsl:text>
      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <FONT color="blue" SIZE="+0" 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="'blue'"/>
+      <xsl:with-param name="size" select="'+0'"/>
+     </xsl:call-template>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
      <xsl:text>)</xsl:text>
     </xsl:when>
@@ -434,7 +495,11 @@
 </xsl:template>
 
 <xsl:template mode="inline" match="m:lambda">
-      <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
+      <xsl:call-template name="mksymbol-1">
+       <xsl:with-param name="symbol" select="'lambda'"/>
+       <xsl:with-param name="color" select="'red'"/>
+       <xsl:with-param name="size" select="'+2'"/>
+      </xsl:call-template>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <xsl:text>:</xsl:text>
       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
@@ -463,7 +528,11 @@
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
          <!-- &#x03a0; -->
-         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</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="'+2'"/>
+         </xsl:call-template>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
@@ -488,7 +557,11 @@
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
-         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</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="'+2'"/>
+         </xsl:call-template>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
@@ -521,9 +594,11 @@
         <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
        </xsl:call-template>
        <!-- -> -->
-       <FONT color="blue" SIZE="+0" 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="'blue'"/>
+        <xsl:with-param name="size" select="'+2'"/>
+       </xsl:call-template>
        <xsl:apply-templates select="*[position()=3]">
         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
        </xsl:apply-templates>
@@ -1354,7 +1429,11 @@
      <xsl:choose>
      <xsl:when test="$charlength > $framewidth">
        <!-- &#x03bb; -->
-       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
+       <xsl:call-template name="mksymbol-1">
+        <xsl:with-param name="symbol" select="'lambda'"/>
+        <xsl:with-param name="color" select="'red'"/>
+        <xsl:with-param name="size" select="'+2'"/>
+       </xsl:call-template>
        <xsl:apply-templates select="m:bvar/m:ci"/>
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">