X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=de2d3c16344df6b3463dd240ac05c7ba156f17f8;hp=6ab6ffe1fcfbc51f201b94adcee89a14ff22d278;hpb=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6ab6ffe1f..4a801a654 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -860,7 +860,7 @@ which generates the toplevel element (see for instance xlink) -->
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <xsl:for-each select="piecewise/piece">
+         <xsl:for-each select="m:piecewise/m:piece">
          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
          <m:mtr>
           <m:mtd>
@@ -910,7 +910,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>OF</m:mo>
-        <xsl:for-each select="piecewise/piece">
+        <xsl:for-each select="m:piecewise/m:piece">
          <xsl:choose>
          <xsl:when test="position() != 1">
           <m:mo stretchy="false">|</m:mo>
@@ -1124,7 +1124,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mrow>
               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-              <xsl:apply-templates select="*[position()=3]"/>
+              <!-- the last child is either the expected type, if provided,-->
+              <!-- or the synthesized type.                                -->
+              <xsl:apply-templates select="*[position()=last()]"/>
               <m:mrow>
                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
                <m:mtext mathcolor="Green">(explain)</m:mtext>
@@ -1145,23 +1147,40 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:variable name="hidedetails">
+            <m:mrow>
+             <m:mphantom>
+              <m:mtext>_</m:mtext>
+             </m:mphantom>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
+            </m:mrow>
+          </xsl:variable>
           <m:mtr>
            <m:mtd>
             <m:mrow>
              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
              <xsl:apply-templates select="*[position()=3]"/>
-             <m:mrow>
-              <m:mphantom>
-               <m:mtext>_</m:mtext>
-              </m:mphantom>
-              <xsl:if test="$test">
-               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
-              </xsl:if>
-             </m:mrow>
+             <xsl:if test="not(*[4])">
+              <xsl:copy-of select="$hidedetails"/>
+             </xsl:if>
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:if test="*[4]">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=4]"/>
+              <xsl:copy-of select="$hidedetails"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:if>
          </m:mtable>
         </xsl:variable>
         <xsl:choose>
@@ -1188,7 +1207,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mrow>
               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-              <xsl:apply-templates select="*[position()=3]"/>
+              <!-- the last child is either the expected type, if provided,-->
+              <!-- or the synthesized type.                                -->
+              <xsl:apply-templates select="*[position()=last()]"/>
               <m:mrow>
                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
                <m:mtext mathcolor="Green">(explain)</m:mtext>
@@ -1209,23 +1230,40 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:variable name="hidedetails">
+            <m:mrow>
+             <m:mphantom>
+              <m:mtext>_</m:mtext>
+             </m:mphantom>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
+            </m:mrow>
+          </xsl:variable>
           <m:mtr>
            <m:mtd>
             <m:mrow>
              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
              <xsl:apply-templates select="*[position()=3]"/>
-             <m:mrow>
-              <m:mphantom>
-               <m:mtext>_</m:mtext>
-              </m:mphantom>
-              <xsl:if test="$test">
-               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
-              </xsl:if>
-             </m:mrow>
+             <xsl:if test="not(*[4])">
+              <xsl:copy-of select="$hidedetails"/>
+             </xsl:if>
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:if test="*[4]">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=4]"/>
+              <xsl:copy-of select="$hidedetails"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:if>
          </m:mtable>
         </xsl:variable>
         <xsl:choose>
@@ -2100,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:param name="nosibling" select="0"/>
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <xsl:value-of select="$incurrent_length"/>
+   <!-- tremendous bug fixed. An empty element can still have siblings!!! -->
+   <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
+   <xsl:choose>
+    <xsl:when test="string($siblength) = &quot;&quot;">
+     <xsl:value-of select="$incurrent_length"/>
+    </xsl:when>
+    <xsl:otherwise>
+      <xsl:value-of select="number($siblength)"/>
+    </xsl:otherwise>
+   </xsl:choose>
   </xsl:when>
   <xsl:otherwise>
     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/><xsl:with-param name="nosibling" select="0"/></xsl:apply-templates></xsl:variable>