<xsl:if test="@id">
<xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
</xsl:if>
+ <xsl:variable name="id" select="m:csymbol/@id"/>
<xsl:choose>
<!-- FORALL -->
<xsl:when test="$name='forall'">
<!-- ***************************************** -->
<!-- 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) -->
+ <!-- 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: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 can 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 can 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 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 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 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 details)</m:mtext>
- </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'">