New: expected types (in the sense of Yann Coscoy) now availables for

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6ab6ffe1fcfbc51f201b94adcee89a14ff22d278..d0167047317b8901047dd8599675aa46f03631a5 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1124,7 +1124,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mrow>
               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-              <xsl:apply-templates select="*[position()=3]"/>
+              <!-- the last child is either the expected type, if provided,-->
+              <!-- or the synthesized type.                                -->
+              <xsl:apply-templates select="*[position()=last()]"/>
               <m:mrow>
                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
                <m:mtext mathcolor="Green">(explain)</m:mtext>
@@ -1145,23 +1147,40 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:variable name="hidedetails">
+            <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>
+          </xsl:variable>
           <m:mtr>
            <m:mtd>
             <m:mrow>
              <m:mtext mathcolor="Red">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>
+             <xsl:if test="not(*[4])">
+              <xsl:copy-of select="$hidedetails"/>
+             </xsl:if>
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:if test="*[4]">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=4]"/>
+              <xsl:copy-of select="$hidedetails"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:if>
          </m:mtable>
         </xsl:variable>
         <xsl:choose>
@@ -1188,7 +1207,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mrow>
               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-              <xsl:apply-templates select="*[position()=3]"/>
+              <!-- the last child is either the expected type, if provided,-->
+              <!-- or the synthesized type.                                -->
+              <xsl:apply-templates select="*[position()=last()]"/>
               <m:mrow>
                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
                <m:mtext mathcolor="Green">(explain)</m:mtext>
@@ -1209,23 +1230,40 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:variable name="hidedetails">
+            <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>
+          </xsl:variable>
           <m:mtr>
            <m:mtd>
             <m:mrow>
              <m:mtext mathcolor="Red">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>
+             <xsl:if test="not(*[4])">
+              <xsl:copy-of select="$hidedetails"/>
+             </xsl:if>
             </m:mrow>
            </m:mtd>
           </m:mtr>
+          <xsl:if test="*[4]">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[position()=4]"/>
+              <xsl:copy-of select="$hidedetails"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:if>
          </m:mtable>
         </xsl:variable>
         <xsl:choose>