From a38dce333847f6a1eaed563f7a2260e1cfc1ff2e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 11 Jun 2002 10:19:54 +0000
Subject: [PATCH] New: expected types (in the sense of Yann Coscoy) now
 availables for MathML Content and MathML Presentation. HTML support is still
 missing (and bugs may have been introduced when expected types are present)

---
 helm/style/content_to_html.xsl |  3 +-
 helm/style/mmlextension.xsl    | 74 +++++++++++++++++++++++++---------
 helm/style/objcontent.xsl      |  2 +-
 helm/style/proofs.xsl          |  4 +-
 4 files changed, 61 insertions(+), 22 deletions(-)

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 01b2a41cb..dc6d6d7a8 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -407,12 +407,13 @@
       </xsl:choose>
      </xsl:for-each>
     </xsl:when>
-    <!-- proof -->
+    <!-- proof and side_proof -->
     <xsl:when test="$name='proof' or $name='side_proof'">
        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
     </xsl:when>
+    <!-- letin1 -->
     <xsl:when test="$name='letin1'">
      <xsl:text>letin1 (inline error)</xsl:text>
     </xsl:when>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6ab6ffe1f..d01670473 100644
--- 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>
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index b4a0e748d..ceb7a22ba 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -61,7 +61,7 @@
        <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]"/>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 5a34d8a06..1d619260a 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -597,7 +597,7 @@
          <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>
@@ -629,7 +629,7 @@
          <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>
-- 
2.39.2