MathML Content and MathML Presentation. HTML support is still missing
(and bugs may have been introduced when expected types are present)
</xsl:choose>
</xsl:for-each>
</xsl:when>
</xsl:choose>
</xsl:for-each>
</xsl:when>
+ <!-- proof and side_proof -->
<xsl:when test="$name='proof' or $name='side_proof'">
<xsl:apply-templates mode="inline" select="*[position()=2]"/>
<FONT color="red"> proves </FONT>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
</xsl:when>
<xsl:when test="$name='proof' or $name='side_proof'">
<xsl:apply-templates mode="inline" select="*[position()=2]"/>
<FONT color="red"> proves </FONT>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
</xsl:when>
<xsl:when test="$name='letin1'">
<xsl:text>letin1 (inline error)</xsl:text>
</xsl:when>
<xsl:when test="$name='letin1'">
<xsl:text>letin1 (inline error)</xsl:text>
</xsl:when>
<m:mrow>
<m:mtext mathcolor="Red">We can prove</m:mtext>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mrow>
<m:mtext mathcolor="Red">We can 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>
<m:mrow>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mtext mathcolor="Green">(explain)</m:mtext>
</m:mrow>
</m:mtd>
</m:mtr>
</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 details)</m:mtext>
+ </xsl:if>
+ </m:mrow>
+ </xsl:variable>
<m:mtr>
<m:mtd>
<m:mrow>
<m:mtext mathcolor="Red">we proved</m:mtext>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<xsl:apply-templates select="*[position()=3]"/>
<m:mtr>
<m:mtd>
<m:mrow>
<m:mtext mathcolor="Red">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>
- <xsl:if test="$test">
- <m:mtext mathcolor="Green">(hide 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>
</m:mrow>
</m:mtd>
</m:mtr>
+ <xsl:if test="*[4]">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext mathcolor="Red">that is equivalent 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>
</m:mtable>
</xsl:variable>
<xsl:choose>
<m:mrow>
<m:mtext mathcolor="Red">We can prove</m:mtext>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mrow>
<m:mtext mathcolor="Red">We can 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>
<m:mrow>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mtext mathcolor="Green">(explain)</m:mtext>
</m:mrow>
</m:mtd>
</m:mtr>
</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 details)</m:mtext>
+ </xsl:if>
+ </m:mrow>
+ </xsl:variable>
<m:mtr>
<m:mtd>
<m:mrow>
<m:mtext mathcolor="Red">we proved</m:mtext>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<xsl:apply-templates select="*[position()=3]"/>
<m:mtr>
<m:mtd>
<m:mrow>
<m:mtext mathcolor="Red">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>
- <xsl:if test="$test">
- <m:mtext mathcolor="Green">(hide 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>
</m:mrow>
</m:mtd>
</m:mtr>
+ <xsl:if test="*[4]">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext mathcolor="Red">that is equivalent 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>
</m:mtable>
</xsl:variable>
<xsl:choose>
<xsl:attribute name="name">
<xsl:value-of select="@name"/>
</xsl:attribute>
<xsl:attribute name="name">
<xsl:value-of select="@name"/>
</xsl:attribute>
- <xsl:attribute name="helm-xref">
+ <xsl:attribute name="helm:xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
<xsl:apply-templates select="*[1]"/>
<xsl:value-of select="@id"/>
</xsl:attribute>
<xsl:apply-templates select="*[1]"/>
<m:csymbol>full_or_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[7]"/>
<xsl:apply-templates mode="pure"
<m:csymbol>full_or_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[7]"/>
<xsl:apply-templates mode="pure"
- select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+ select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
<m:apply>
<m:csymbol>left_case</m:csymbol>
<m:bvar>
<m:apply>
<m:csymbol>left_case</m:csymbol>
<m:bvar>
<m:csymbol>or_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[7]"/>
<xsl:apply-templates mode="pure"
<m:csymbol>or_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[7]"/>
<xsl:apply-templates mode="pure"
- select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+ select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
<xsl:apply-templates mode="pure" select="*[5]"/>
<xsl:apply-templates mode="pure" select="*[6]"/>
</m:apply>
<xsl:apply-templates mode="pure" select="*[5]"/>
<xsl:apply-templates mode="pure" select="*[6]"/>
</m:apply>