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

diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 06e23deca..46fc61b24 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,42 @@
 
 <!-- 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:eq|m:leq|m:lt|m:geq|m:gt">
+  <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
+  <xsl:choose>
+  <xsl:when test="$uri != ''">
+   <a href="{$uri}">
+    <xsl:call-template name="mksymbol-init">
+     <xsl:with-param name="symbol" select="local-name(.)"/>
+    </xsl:call-template>
+   </a>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:call-template name="mksymbol-init">
+     <xsl:with-param name="symbol" select="local-name(.)"/>
+   </xsl:call-template>
+  </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 +302,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>