From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 11 Jun 2002 10:19:54 +0000 (+0000)
Subject: New: expected types (in the sense of Yann Coscoy) now availables for
X-Git-Tag: V_0_3_0_debian_8~52
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a38dce333847f6a1eaed563f7a2260e1cfc1ff2e;p=helm.git

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)
---

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>