First version using maction/toggle to navigate proofs.

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 8566c972630e3435160cb4cc772c425169edb34b..bb13c876ebcd93bf38997b2c190d2a0b3e258747 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -44,6 +44,8 @@ which generates the toplevel element (see for instance xlink) -->
 
 <xsl:import href="mmltheoryextension.xsl"/>
 
+<xsl:param name="explodeall" select="false()"/>
+
 <!--***********************************************************************-->
 <!-- Parameter affecting line-breaking                                     -->
 <!--***********************************************************************-->
@@ -979,6 +981,23 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- ***************************************** -->
       <!-- PROOF -->
       <xsl:when test="$name='proof'">
+       <m:maction actiontype="toggle">
+        <!-- CSC: next if until the annotationHelper can handle mactions -->
+        <xsl:if test="not($explodeall)">
+         <!-- Details hided (default) -->
+         <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>
+        </xsl:if>
+        <!-- Show details -->
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
@@ -990,13 +1009,20 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we proved </m:mtext>
+            <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">(hide&#x00a0;details)</m:mtext>
+            </m:mrow>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
+       </m:maction>
       </xsl:when>
       <!-- LETIN1 -->
       <xsl:when test="$name='letin1'">