X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=65a2b4612f01e90d00ffcadd01d3261bc50e3a81;hpb=564808f227d45537df5061e05d81fcc70cb06f9d;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 65a2b4612..4a801a654 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -181,11 +181,54 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:for-each select="Conjecture">
       <m:mtr>
        <m:mtd>
-        <m:mrow>
+        <m:mrow helm:xref="{@helm:xref}">
          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+         <xsl:for-each select="Decl|Def|Hidden">
+          <xsl:choose>
+           <xsl:when test="name(.)='Decl'">
+            <m:mrow helm:xref="{@helm:xref}">
+             <xsl:choose>
+              <xsl:when test="@name">
+               <m:mi><xsl:value-of select="@name"/></m:mi>
+              </xsl:when>
+              <xsl:otherwise>
+               <m:mi>_</m:mi>
+              </xsl:otherwise>
+             </xsl:choose>
+             <m:mo>:</m:mo>
+             <xsl:apply-templates select="./*[1]"/>
+            </m:mrow>
+           </xsl:when>
+           <xsl:when test="name(.)='Def'">
+            <m:mrow helm:xref="{@helm:xref}">
+             <xsl:choose>
+              <xsl:when test="@name">
+               <m:mi><xsl:value-of select="@name"/></m:mi>
+              </xsl:when>
+              <xsl:otherwise>
+               <m:mi>_</m:mi>
+              </xsl:otherwise>
+             </xsl:choose>
+             <m:mo>:=</m:mo>
+             <xsl:apply-templates select="./*[1]"/>
+            </m:mrow>
+           </xsl:when>
+           <xsl:otherwise>
+            <m:mrow helm:xref="{@helm:xref}">
+             <m:mi>_</m:mi>
+             <m:mo>:?</m:mo>
+             <m:mi>_</m:mi>
+            </m:mrow>
+           </xsl:otherwise>
+          </xsl:choose>
+          <xsl:if test="not (position() = last())">
+           <m:mo>;</m:mo>
+          </xsl:if>
+         </xsl:for-each>
+         <m:mo>|-</m:mo>
          <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
-         <m:mtext>:</m:mtext>
-         <xsl:apply-templates select="./*[1]"/>
+         <m:mo>:</m:mo>
+         <xsl:apply-templates select="./Goal/*[1]"/>
         </m:mrow>
        </m:mtd>
       </m:mtr>
@@ -365,22 +408,26 @@ which generates the toplevel element (see for instance xlink) -->
 
 <xsl:template match="Sequent">
  <xsl:variable name="rowlines">
-  <xsl:for-each select="Declaration|Definition">
+  <xsl:for-each select="Decl|Def">
    <xsl:if test="position() != last()">
     <xsl:text>none </xsl:text>
    </xsl:if>
   </xsl:for-each>
   <xsl:text>solid</xsl:text>
  </xsl:variable>
+ <xsl:variable name="no" select="@no"/>
     <m:math>
+     <m:mi><xsl:text>?</xsl:text><xsl:value-of select="$no"/></m:mi>
+     <m:mo>:</m:mo>
+     <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
-      <xsl:for-each select="Declaration|Definition">
+      <xsl:for-each select="Decl|Def">
        <m:mtr>
         <m:mtd>
-         <m:mrow>
+         <m:mrow helm:xref="{@helm:xref}">
           <m:mi><xsl:value-of select="@name"/></m:mi>
           <xsl:choose>
-           <xsl:when test="name(.) = 'Declaration'">
+           <xsl:when test="name(.) = 'Decl'">
             <m:mo>:</m:mo>
            </xsl:when>
            <xsl:otherwise>
@@ -392,7 +439,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtd>
        </m:mtr>
       </xsl:for-each>
-      <xsl:if test="not(Declaration|Definition)">
+      <xsl:if test="not(Decl|Def)">
       <m:mtr>
        <m:mtd>
         <m:mrow>
@@ -470,6 +517,15 @@ which generates the toplevel element (see for instance xlink) -->
      </xsl:if>
      <xsl:variable name="id" select="m:csymbol/@id"/>
      <xsl:choose>
+      <!-- META -->
+      <xsl:when test="$name='meta'">
+       <m:mrow>
+        <xsl:apply-templates select="*[position()=2]"/>
+        <m:mfenced open="[" close="]" separators=";">
+         <xsl:apply-templates select="*[position()>2]"/>
+        </m:mfenced>
+       </m:mrow>
+      </xsl:when>
       <!-- FORALL -->
       <xsl:when test="$name='forall'">
        <xsl:choose>
@@ -804,7 +860,7 @@ which generates the toplevel element (see for instance xlink) -->
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <xsl:for-each select="piecewise/piece">
+         <xsl:for-each select="m:piecewise/m:piece">
          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
          <m:mtr>
           <m:mtd>
@@ -854,7 +910,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>OF</m:mo>
-        <xsl:for-each select="piecewise/piece">
+        <xsl:for-each select="m:piecewise/m:piece">
          <xsl:choose>
          <xsl:when test="position() != 1">
           <m:mo stretchy="false">|</m:mo>
@@ -1068,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>
@@ -1089,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>
@@ -1132,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>
@@ -1153,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>
@@ -2044,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:param name="nosibling" select="0"/>
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <xsl:value-of select="$incurrent_length"/>
+   <!-- tremendous bug fixed. An empty element can still have siblings!!! -->
+   <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
+   <xsl:choose>
+    <xsl:when test="string($siblength) = &quot;&quot;">
+     <xsl:value-of select="$incurrent_length"/>
+    </xsl:when>
+    <xsl:otherwise>
+      <xsl:value-of select="number($siblength)"/>
+    </xsl:otherwise>
+   </xsl:choose>
   </xsl:when>
   <xsl:otherwise>
     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/><xsl:with-param name="nosibling" select="0"/></xsl:apply-templates></xsl:variable>