X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fhtml_set.xsl;h=78f4a5b9ea98e0c01ed0b1c9d7bd8c40b3fc2dbb;hb=083c36a4acd76127530b9af3d4c6c311f447d79b;hp=5b50211df2731a16af83b354ee2b20225dfe3eab;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git

diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 5b50211df..78f4a5b9e 100644
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -32,8 +32,6 @@
 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
 <!--***********************************************************************--> 
 
-<xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
-
 <!-- IN -->
 
  <xsl:template match="m:apply[m:in]">
@@ -59,7 +57,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#206;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -73,7 +71,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#206;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -102,7 +100,7 @@
      <xsl:call-template name="make_indent">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#207;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
      </xsl:apply-templates>
@@ -111,7 +109,7 @@
     <xsl:otherwise>
      <xsl:text>(</xsl:text>
      <xsl:apply-templates select="*[2]"/>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#207;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
     </xsl:otherwise>
@@ -128,7 +126,7 @@
   </xsl:variable>
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" color="blue">&#198;</FONT>
+    <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:variable name="charlength">
@@ -231,7 +229,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#199;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -245,7 +243,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#199;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -278,7 +276,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#200;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -292,7 +290,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#200;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -324,7 +322,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#205;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -338,7 +336,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#205;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -370,7 +368,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#204;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -384,7 +382,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#204;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>