- added method to check for an attribute in a given namespace

[helm.git] / helm / style / mmlextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 75c8a745be217d541858131a263a29824fa8f94d..eb928b41f183b9f8685525b2898a883ed642a766 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -414,6 +414,7 @@ which generates the toplevel element (see for instance xlink) -->
      <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'">
@@ -988,8 +989,12 @@ 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)">
+        <!-- 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) -->
          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
           <m:mtr>
@@ -1026,7 +1031,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mphantom>
               <m:mtext>_</m:mtext>
              </m:mphantom>
-             <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
             </m:mrow>
            </m:mrow>
           </m:mtd>