]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/content_to_html.xsl
characters in symbol font unified in size
[helm.git] / helm / style / content_to_html.xsl
index b5706d60c29f91a00ce635b5922379261e22c546..07999b6e080b33e14b5fd783860359c8e3b5490e 100644 (file)
    <xsl:choose>
     <!-- FORALL -->
     <xsl:when test="$name='forall'">
-     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
+     <FONT FACE="Symbol" SIZE="+0" color="blue">&#x22;</FONT>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
     </xsl:when>
     <xsl:when test="$name='prod'">
-     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
+     <FONT FACE="Symbol" SIZE="+0" color="blue">&#x00d5;</FONT>
      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
     <xsl:when test="$name='arrow'">
      <xsl:text>(</xsl:text>
      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <FONT color="blue" SIZE="+2" FACE="symbol">
+     <FONT color="blue" SIZE="+0" FACE="symbol">
       <xsl:text>&#x00ae;</xsl:text>
      </FONT>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
        </xsl:when> 
       </xsl:choose>
       <xsl:apply-templates mode="inline" select="."/>
-      <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
+      <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
       <xsl:apply-templates mode="inline"
            select="following-sibling::*[position()= 1]"/>
      </xsl:for-each>
 </xsl:template>
 
 <xsl:template mode="inline" match="m:lambda">
-      <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
+      <FONT SIZE="+0" color="red" FACE="symbol">l</FONT>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <xsl:text>:</xsl:text>
       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
          <!-- &#x03a0; -->
-         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
+         <FONT FACE="Symbol" SIZE="+0" color="blue">&#x22;</FONT>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
-         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
+         <FONT FACE="Symbol" SIZE="+0" color="blue">&#x00d5;</FONT>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
        </xsl:call-template>
        <!-- -> -->
-       <FONT color="blue" SIZE="+2" FACE="symbol">
+       <FONT color="blue" SIZE="+0" FACE="symbol">
         <xsl:text>&#x00ae;</xsl:text>
        </FONT>
        <xsl:apply-templates select="*[position()=3]">
             </xsl:otherwise>
             </xsl:choose>
             <xsl:apply-templates select="."/>
-            <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
+            <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
             <xsl:apply-templates select="following-sibling::*[position()= 1]">
              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
             </xsl:apply-templates>
      <xsl:choose>
      <xsl:when test="$charlength > $framewidth">
        <!-- &#x03bb; -->
-       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
+       <FONT SIZE="+0" color="red" FACE="symbol">l</FONT>
        <xsl:apply-templates select="m:bvar/m:ci"/>
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">