BUG FIXED:

An maction with only one child does not have the same semantic
of an mrow. E.g.: when I click to un-expand a node, the first enclosing
maction is the one I am acting on. If it has only one child, nothing
happens. So, if an maction with only one child is put inside an maction with
two children, the inner one stops any possibility to unexpand the outer one.

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index eb928b41f183b9f8685525b2898a883ed642a766..6dce30b65a73b02bf009013469380fd523eb18a0 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -988,58 +988,71 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- ***************************************** -->
       <!-- PROOF -->
       <xsl:when test="$name='proof'">
-       <m:maction actiontype="toggle">
         <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
         <xsl:variable name="test" select="(not($explodeall)) and
           (not(preceding-sibling::*[1]/text()='letin1')) and
           (not(preceding-sibling::*[1]/text()='rw_step')) and
           (not(name(..)='m:lambda'))"/>
-        <xsl:if test="$test">
-         <!-- Details hided (default) -->
+        <xsl:variable name="hidden_details">
+         <xsl:if test="$test">
+          <!-- Details hided (default) -->
+          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</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>
+               <m:mtext mathcolor="Green">(explain)</m:mtext>
+              </m:mrow>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </m:mtable>
+         </xsl:if>
+        </xsl:variable>
+        <xsl:variable name="shown_details">
+         <!-- Show details -->
          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
           <m:mtr>
            <m:mtd>
             <m:mrow>
-             <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
+             <xsl:apply-templates select="*[position()=2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mtext mathcolor="Maroon">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>
-              <m:mtext mathcolor="Green">(explain)</m:mtext>
+              <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>
             </m:mrow>
            </m:mtd>
           </m:mtr>
          </m:mtable>
-        </xsl:if>
-        <!-- Show details -->
-        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-         <m:mtr>
-          <m:mtd>
-           <m:mrow>
-            <xsl:apply-templates select="*[position()=2]"/>
-           </m:mrow>
-          </m:mtd>
-         </m:mtr>
-         <m:mtr>
-          <m:mtd>
-           <m:mrow>
-            <m:mtext mathcolor="Maroon">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>
-           </m:mrow>
-          </m:mtd>
-         </m:mtr>
-        </m:mtable>
-       </m:maction>
+        </xsl:variable>
+        <xsl:choose>
+         <xsl:when test="$test">
+          <m:maction actiontype="toggle">
+           <xsl:copy-of select="$hidden_details"/>
+           <xsl:copy-of select="$shown_details"/>
+          </m:maction>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:copy-of select="$shown_details"/>
+         </xsl:otherwise>
+        </xsl:choose>
       </xsl:when>
       <!-- LETIN1 -->
       <xsl:when test="$name='letin1'">