X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fhtml_init.xsl;h=d3c9d19926ef18b55196995aa961e34eb8207c4c;hb=0db688b75474e712a3ec7f05180b0cb06002fae2;hp=06e23deca32262733225d7b0e43a0338e9de37a8;hpb=19681f7b0c71fbb8c9e3442c0880533731094046;p=helm.git

diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 06e23deca..d3c9d1992 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -62,6 +62,9 @@
       </xsl:when>
       <xsl:when test="$symbol = 'times'">
        <xsl:value-of select="'&#42;'"/>
+      </xsl:when> 
+      <xsl:when test="$symbol = 'divide'">
+       <xsl:value-of select="'&#47;'"/>
       </xsl:when>
       <xsl:when test="$symbol = 'minus'">
        <xsl:value-of select="'&#45;'"/>
@@ -114,6 +117,9 @@
       <xsl:when test="$symbol = 'times'">
        <xsl:value-of select="'&#8727;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'divide'">
+       <xsl:value-of select="'&#47;'"/>
+      </xsl:when>
       <xsl:when test="$symbol = 'minus'">
        <xsl:value-of select="'&#8722;'"/>
       </xsl:when>
@@ -143,8 +149,24 @@
 
 <!-- INLINE MODE : BASIC OPERATORS -->
 
+<xsl:template mode="inline" match="m:infinity">
+ <xsl:choose>
+  <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
+   <FONT FACE="symbol" color="'blue'">
+    <xsl:value-of select="'&#165;'"/>
+   </FONT>
+  </xsl:when>
+  <xsl:otherwise>
+   <FONT color="'blue'">
+    <!-- VERIFICARE -->
+    <xsl:value-of select="'&#165;'"/>
+   </FONT>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
  <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
-       |m:geq|m:gt|m:plus|m:times]">
+       |m:geq|m:gt|m:plus|m:times|m:divide]">
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
@@ -262,7 +284,7 @@
 <!-- BASIC OPERATORS -->
 
  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
-       |m:geq|m:gt|m:plus|m:times]">
+       |m:geq|m:gt|m:plus|m:times|m:divide]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>