X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=7aeec143f15f8a2cf3b11cbb934ae7aa900fee91;hb=ddce32beebecf9d965e6ad991a08368f52cd9ea1;hp=6e766e3528c6ecf705b849896e854901a839d1c4;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6e766e352..7aeec143f 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -183,9 +183,52 @@ which generates the toplevel element (see for instance xlink) -->
        <m:mtd>
         <m:mrow>
          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+         <xsl:for-each select="Decl|Def|Hidden">
+          <xsl:choose>
+           <xsl:when test="name(.)='Decl'">
+            <m:mrow>
+             <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>
+             <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>
+             <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>
@@ -372,7 +415,11 @@ which generates the toplevel element (see for instance xlink) -->
   </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="Decl|Def">
        <m:mtr>
@@ -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>