X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlnotation.xsl;h=5cf944e72ec54c20b16c344de1b82859b8b4a691;hb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;hp=babc7f41db0ff8e37626b736269fd2f05e406236;hpb=c8c75f895d51cfbc257260859653a68f74117179;p=helm.git

diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl
index babc7f41d..5cf944e72 100644
--- a/helm/style/mmlnotation.xsl
+++ b/helm/style/mmlnotation.xsl
@@ -96,19 +96,11 @@
  </xsl:choose>
 </xsl:template>
 
-
-<xsl:template match = "m:apply[m:and[1]|m:or[1]
-          |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
-          |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
-          |m:prsubset|m:setdiff[1]]">
+<!-- apply-imports without parenthesis -->
+<xsl:template match = "m:apply[m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]|m:in[1]|
+                               m:subset[1]|m:prsubset[1]]">
  <xsl:variable name="symbol">
   <xsl:choose>
-   <xsl:when test="m:and[1]">
-    <xsl:value-of select="'&#8743;'"/>
-   </xsl:when>
-   <xsl:when test="m:or[1]">
-    <xsl:value-of select="'&#8744;'"/>
-   </xsl:when>
    <xsl:when test="m:geq[1]">
     <xsl:value-of select="'&#8805;'"/>
    </xsl:when>
@@ -121,9 +113,6 @@
    <xsl:when test="m:lt[1]">
     <xsl:value-of select="'&#60;&#32;'"/>
    </xsl:when>
-   <xsl:when test="m:eq[1]">
-    <xsl:value-of select="'&#61;'"/>
-   </xsl:when>
    <xsl:when test="m:in[1]">
     <xsl:value-of select="'&#x02208;'"/>
    </xsl:when>
@@ -133,6 +122,69 @@
    <xsl:when test="m:prsubset[1]">
     <xsl:value-of select="'&#x02282;'"/>
    </xsl:when>
+  </xsl:choose>
+ </xsl:variable>
+ <xsl:variable name="charlength">
+  <xsl:apply-templates select="*[1]" mode="charcount"/>
+ </xsl:variable>
+ <xsl:choose>
+  <xsl:when test="$charlength >= $framewidth">
+   <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+    <xsl:if test="@id">
+     <xsl:attribute name="xref">
+      <xsl:value-of select="@id"/>
+     </xsl:attribute>
+    </xsl:if>    
+    <m:mtr>
+     <m:mtd>
+      <m:mrow>
+       <m:mo stretchy="false">(</m:mo>
+       <xsl:apply-templates select="*[position()=2]"/>
+      </m:mrow>
+     </m:mtd>
+    </m:mtr>
+    <xsl:for-each select = "*[position()>2]">
+     <m:mtr>
+      <m:mtd>
+       <m:mrow>
+        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+        <m:mo>
+         <xsl:if test="*[1]/@id">
+          <xsl:attribute name="xref">
+           <xsl:value-of select="*[1]/@id"/>
+          </xsl:attribute>
+         </xsl:if><xsl:value-of select="$symbol"/></m:mo>
+        <xsl:apply-templates select="."/>
+       </m:mrow>
+      </m:mtd>
+     </m:mtr>
+    </xsl:for-each>
+    <m:mtr>
+     <m:mtd>
+      <m:mrow>
+       <m:mo stretchy="false">)</m:mo>
+      </m:mrow>
+     </m:mtd>
+    </m:mtr>
+   </m:mtable>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-imports/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- apply-imports with parenthesis -->
+<xsl:template match = "m:apply[m:and[1]|m:or[1]
+          |m:intesect[1]|m:union[1]|m:setdiff[1]]">
+ <xsl:variable name="symbol">
+  <xsl:choose>
+   <xsl:when test="m:and[1]">
+    <xsl:value-of select="'&#8743;'"/>
+   </xsl:when>
+   <xsl:when test="m:or[1]">
+    <xsl:value-of select="'&#8744;'"/>
+   </xsl:when>
    <xsl:when test="m:intersect[1]">
     <xsl:value-of select="'&#x022C2;'"/>
    </xsl:when>
@@ -189,7 +241,11 @@
    </m:mtable>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-imports/>
+<!-- Added mfenced because apply-imports doesn't support with-param for 
+     precedence  (XSLT 2.0) -->
+   <m:mfenced separators=" ">
+    <xsl:apply-imports/>
+   </m:mfenced>
   </xsl:otherwise>
  </xsl:choose>
 </xsl:template>