X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=f92205008f00708b89415de1a5adb9c55ed34896;hpb=e271d6d3bf82d56b6a72717759b5319dcf7c67f8;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index f92205008..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>
@@ -364,15 +407,27 @@ which generates the toplevel element (see for instance xlink) -->
 <!-- SEQUENT -->
 
 <xsl:template match="Sequent">
+ <xsl:variable name="rowlines">
+  <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:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
-      <xsl:for-each select="Declaration|Definition">
+     <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="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>
@@ -384,13 +439,15 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtd>
        </m:mtr>
       </xsl:for-each>
+      <xsl:if test="not(Decl|Def)">
       <m:mtr>
        <m:mtd>
         <m:mrow>
-         <m:mtext>========================================</m:mtext>
+         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         </m:mrow>
        </m:mtd>
       </m:mtr>
+      </xsl:if>
       <m:mtr>
        <m:mtd>
         <m:mrow>
@@ -460,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>
@@ -794,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>
@@ -844,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>
@@ -1058,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>
@@ -1079,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>
@@ -1122,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>
@@ -1143,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>
@@ -2034,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>