X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fmmlextension.xsl;h=6dce30b65a73b02bf009013469380fd523eb18a0;hb=d4dd07ecc4191d9dac83b5d4d23dfc61c4492d77;hp=049398f9a9539c1d1492d252ad507cd49897e2c2;hpb=3d585511751044f308125da7a71d70e29cc6ca60;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 049398f9a..6dce30b65 100644
--- 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'">
@@ -987,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'">
@@ -1536,8 +1550,8 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mo stretchy="false">[</m:mo>
         <xsl:apply-templates select="*[4]"/>
         <m:mo mathcolor="green">
-         <xsl:if test="@id != ''">
-          <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
          </xsl:if>&#8592;</m:mo>
         <xsl:apply-templates select="*[2]"/>
         <m:mo stretchy="false">]</m:mo>
@@ -1546,8 +1560,8 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:when test="$name='lift'">
         <m:msup>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8593;</m:mo>
 	 <xsl:apply-templates select="*[2]"/>
         </m:msup>
@@ -1561,8 +1575,8 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:when test="$name='lift_with_base'">
         <m:msubsup>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8593;</m:mo>
 	 <xsl:apply-templates select="*[3]"/>
 	 <xsl:apply-templates select="*[4]"/>
@@ -1578,8 +1592,8 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[2]"/>
         <m:munder>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8594;</m:mo>
           <m:mi mathcolor="green">&#946;</m:mi>
         </m:munder>
@@ -1590,8 +1604,8 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[2]"/>
         <m:munderover>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8594;</m:mo>
           <m:mi mathcolor="green">&#946;</m:mi>
           <m:mi mathcolor="green">*</m:mi>
@@ -1603,8 +1617,8 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[2]"/>
         <m:munder>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8658;</m:mo>
           <m:mi mathcolor="green">&#946;</m:mi>
         </m:munder>
@@ -1615,8 +1629,8 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[2]"/>
         <m:munderover>
          <m:mo mathcolor="green">
-          <xsl:if test="@id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8658;</m:mo>
           <m:mi mathcolor="green">&#946;</m:mi>
           <m:mi mathcolor="green">*</m:mi>
@@ -1626,8 +1640,8 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- forgetful -->
       <xsl:when test="$name='forgetful'">
        <m:mfenced open="|" close="|">
-        <xsl:if test="@id != ''">
-         <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
         </xsl:if>
         <xsl:apply-templates select="*[2]"/>
        </m:mfenced>
@@ -1636,16 +1650,16 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:when test="$name='isomorphic'">
         <xsl:apply-templates select="*[2]"/>
         <m:mo mathcolor="green">
-         <xsl:if test="@id != ''">
-          <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
          </xsl:if>&#8773;</m:mo>
         <xsl:apply-templates select="*[3]"/>
       </xsl:when>
       <!-- interp -->
       <xsl:when test="$name='forgetful'">
        <m:mfenced open="[" close="]">
-        <xsl:if test="@id != ''">
-         <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
         </xsl:if>
         <xsl:apply-templates select="*[2]"/>
        </m:mfenced>