From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 4 Apr 2001 09:47:02 +0000 (+0000)
Subject: characters in symbol font unified in size
X-Git-Tag: v0_1_2~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=fffff12ad86e979d3a86c43b56ba234d8afa5c2a;p=helm.git

characters in symbol font unified in size
---

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index b5706d60c..07999b6e0 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -140,7 +140,7 @@
    <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"/>
@@ -148,7 +148,7 @@
      <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"/>
@@ -159,7 +159,7 @@
     <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]"/>
@@ -207,7 +207,7 @@
        </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>
@@ -297,7 +297,7 @@
 </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"/>
@@ -326,7 +326,7 @@
        <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">
@@ -351,7 +351,7 @@
       <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">
@@ -384,7 +384,7 @@
         <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]">
@@ -486,7 +486,7 @@
             </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>
@@ -1051,7 +1051,7 @@
      <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">
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index f8930ed05..f6fad1619 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -76,7 +76,7 @@
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
   <a href="{$uri}">
-   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
+   <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
     <xsl:value-of select="$symbol"/>
    </FONT>
   </a>
@@ -93,7 +93,7 @@
   <xsl:choose>
    <xsl:when test="count(child::*)=2">
     <a href="{$uri}">
-    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
+    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates mode="inline" select="*[2]"/>
    </xsl:when>
@@ -101,7 +101,7 @@
     <xsl:text>(</xsl:text>
     <xsl:apply-templates mode="inline" select="*[2]"/>
     <a href="{$uri}">
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
+     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates mode="inline" select="*[3]"/>
     <xsl:text>)</xsl:text>
@@ -116,7 +116,7 @@
    <xsl:value-of select="m:not/@definitionURL"/>
   </xsl:variable>
      <a href="{$uri}">
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#216;</FONT>
+     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#216;</FONT>
      </a>
      <xsl:apply-templates mode="inline" select="*[2]"/>
  </xsl:template>
@@ -128,7 +128,7 @@
    <xsl:value-of select="m:exists/@definitionURL"/>
   </xsl:variable>
   <a href="{$uri}">
-   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#36;</FONT>
+   <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#36;</FONT>
   </a>
   <xsl:apply-templates select="m:bvar/m:ci"/>
   <xsl:text>:</xsl:text>
@@ -196,7 +196,7 @@
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
      <a href="{$uri}">
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
+     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
       <xsl:value-of select="$symbol"/>
      </FONT>
      </a>
@@ -222,7 +222,7 @@
   <xsl:choose>
    <xsl:when test="count(child::*)=2">
     <a href="{$uri}">
-    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
+    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates select="*[2]">
      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
@@ -243,7 +243,7 @@
        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
       </xsl:call-template>
       <a href="{$uri}">
-      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
+      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#45;</FONT>
       </a>
       <xsl:apply-templates select="*[3]">
        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -267,7 +267,7 @@
    <xsl:value-of select="m:not/@definitionURL"/>
   </xsl:variable>
      <a href="{$uri}">
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#216;</FONT>
+     <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#216;</FONT>
      </a>
      <xsl:apply-templates select="*[2]"/>
  </xsl:template>
@@ -286,7 +286,7 @@
   <xsl:choose>
     <xsl:when test="$charlength > $framewidth">
      <a href="{$uri}">
-      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#36;</FONT>
+      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#36;</FONT>
      </a>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 3eb826465..224c76088 100644
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -44,7 +44,7 @@
   </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#198;</FONT>
+    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:choose>
@@ -122,7 +122,7 @@
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
   <a href="{$uri}">
-   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
+   <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
     <xsl:value-of select="$symbol"/>
    </FONT>
   </a>
@@ -178,7 +178,7 @@
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
      <a href="{$uri}">
-      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
+      <FONT FACE="symbol" SIZE="+0" mathcolor="blue">
        <xsl:value-of select="$symbol"/>
       </FONT>
      </a>
@@ -204,7 +204,7 @@
   </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#198;</FONT>
+    <FONT FACE="symbol" SIZE="+0" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:variable name="charlength">