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

diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl
index a89a2e4b9..5cf944e72 100644
--- a/helm/style/mmlnotation.xsl
+++ b/helm/style/mmlnotation.xsl
@@ -36,7 +36,7 @@
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:m="http://www.w3.org/1998/Math/MathML">
 
-<xsl:import href="mmlctop.xsl-0.14"/>
+<xsl:import href="mmlctop.xsl"/>
 
 
 <!-- *********************************** -->
@@ -53,7 +53,7 @@
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
     <xsl:if test="@id">
-     <xsl:attribute name="m:xref">
+     <xsl:attribute name="xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
     </xsl:if>    
@@ -72,7 +72,7 @@
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
         <m:mo>
          <xsl:if test="m:in/@id">
-          <xsl:attribute name="m:xref">
+          <xsl:attribute name="xref">
            <xsl:value-of select="m:in/@id"/>
           </xsl:attribute>
          </xsl:if>=</m:mo>
@@ -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>
@@ -151,7 +203,7 @@
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
     <xsl:if test="@id">
-     <xsl:attribute name="m:xref">
+     <xsl:attribute name="xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
     </xsl:if>    
@@ -170,7 +222,7 @@
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
         <m:mo>
          <xsl:if test="*[1]/@id">
-          <xsl:attribute name="m:xref">
+          <xsl:attribute name="xref">
            <xsl:value-of select="*[1]/@id"/>
           </xsl:attribute>
          </xsl:if><xsl:value-of select="$symbol"/></m:mo>
@@ -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>
@@ -199,7 +255,7 @@
   <xsl:when test="count(child::*) = 0">
    <m:mi>
     <xsl:if test="@id">
-     <xsl:attribute name="m:xref">
+     <xsl:attribute name="xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
     </xsl:if>&#x02205;</m:mi>
@@ -218,7 +274,7 @@
           <m:mrow>
            <m:mo stretchy="false">
             <xsl:if test="@id">
-             <xsl:attribute name="m:xref">
+             <xsl:attribute name="xref">
               <xsl:value-of select="@id"/>
              </xsl:attribute>
             </xsl:if>{</m:mo>
@@ -240,7 +296,7 @@
           <m:mrow>
            <m:mo stretchy="false">
             <xsl:if test="@id">
-             <xsl:attribute name="m:xref">
+             <xsl:attribute name="xref">
               <xsl:value-of select="@id"/>
              </xsl:attribute>
             </xsl:if>}</m:mo>
@@ -256,7 +312,7 @@
           <m:mrow>
            <m:mo stretchy="false">
             <xsl:if test="@id">
-             <xsl:attribute name="m:xref">
+             <xsl:attribute name="xref">
               <xsl:value-of select="@id"/>
              </xsl:attribute>
             </xsl:if>{</m:mo>
@@ -285,7 +341,7 @@
           <m:mrow>
            <m:mo stretchy="false">
             <xsl:if test="@id">
-             <xsl:attribute name="m:xref">
+             <xsl:attribute name="xref">
               <xsl:value-of select="@id"/>
              </xsl:attribute>
             </xsl:if>}</m:mo>
@@ -307,7 +363,7 @@
 <xsl:template match = "m:apply[m:card[1]]">
   <m:mfenced open="|" close="|" stretchy="false">
     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
-      <xsl:attribute name="m:xref">
+      <xsl:attribute name="xref">
         <xsl:value-of select="@id"/>
       </xsl:attribute>
     </xsl:if>