X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6ab6ffe1fcfbc51f201b94adcee89a14ff22d278;hb=1cfcea66d7394a785ec439cd6b03497b276918c4;hp=7e9bd1e5f085b1711a8a64458e66c7d9db7f211c;hpb=d88218090d8607c08455ad3f1791441c7b09f49a;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 7e9bd1e5f..6ab6ffe1f 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -181,10 +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>
-         <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
-         <xsl:apply-templates select="./*[1]"/>
+         <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:mo>:</m:mo>
+         <xsl:apply-templates select="./Goal/*[1]"/>
         </m:mrow>
        </m:mtd>
       </m:mtr>
@@ -192,7 +236,7 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtr>
        <m:mtd>
         <m:mrow>
-         <m:mtext>CORRESPONDING PROOF:</m:mtext>
+         <m:mtext>PROOF:</m:mtext>
         </m:mrow>
        </m:mtd>
       </m:mtr>
@@ -360,6 +404,61 @@ which generates the toplevel element (see for instance xlink) -->
     </m:math>
 </xsl:template>
 
+<!-- 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: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 helm:xref="{@helm:xref}">
+          <m:mi><xsl:value-of select="@name"/></m:mi>
+          <xsl:choose>
+           <xsl:when test="name(.) = 'Decl'">
+            <m:mo>:</m:mo>
+           </xsl:when>
+           <xsl:otherwise>
+            <m:mo>:=</m:mo>
+           </xsl:otherwise>
+          </xsl:choose>
+          <xsl:apply-templates select="*[1]"/>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+      </xsl:for-each>
+      <xsl:if test="not(Decl|Def)">
+      <m:mtr>
+       <m:mtd>
+        <m:mrow>
+         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        </m:mrow>
+       </m:mtd>
+      </m:mtr>
+      </xsl:if>
+      <m:mtr>
+       <m:mtd>
+        <m:mrow>
+         <xsl:apply-templates select="Goal/*[1]"/>
+        </m:mrow>
+       </m:mtd>
+      </m:mtr>
+     </m:mtable>
+    </m:math>
+</xsl:template>
+
 <!--**********************-->
 <!--        TERMS         -->
 <!--**********************-->
@@ -414,10 +513,19 @@ which generates the toplevel element (see for instance xlink) -->
     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
     <m:mrow>
      <xsl:if test="@id">
-      <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+      <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
      </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>
@@ -1715,7 +1823,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[4]"/>
         <m:mo mathcolor="Green">
          <xsl:if test="$id != ''">
-          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
          </xsl:if>&#8592;</m:mo>
         <xsl:apply-templates select="*[2]"/>
         <m:mo stretchy="false">]</m:mo>
@@ -1725,7 +1833,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:msup>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8593;</m:mo>
 	 <xsl:apply-templates select="*[2]"/>
         </m:msup>
@@ -1740,7 +1848,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:msubsup>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8593;</m:mo>
 	 <xsl:apply-templates select="*[3]"/>
 	 <xsl:apply-templates select="*[4]"/>
@@ -1757,7 +1865,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:munder>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8594;</m:mo>
           <m:mi mathcolor="Green">&#946;</m:mi>
         </m:munder>
@@ -1769,7 +1877,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:munderover>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8594;</m:mo>
           <m:mi mathcolor="Green">&#946;</m:mi>
           <m:mi mathcolor="Green">*</m:mi>
@@ -1782,7 +1890,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:munder>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8658;</m:mo>
           <m:mi mathcolor="Green">&#946;</m:mi>
         </m:munder>
@@ -1794,7 +1902,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:munderover>
          <m:mo mathcolor="Green">
           <xsl:if test="$id != ''">
-           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
           </xsl:if>&#8658;</m:mo>
           <m:mi mathcolor="Green">&#946;</m:mi>
           <m:mi mathcolor="Green">*</m:mi>
@@ -1805,7 +1913,7 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:when test="$name='forgetful'">
        <m:mfenced open="|" close="|">
         <xsl:if test="$id != ''">
-         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
         </xsl:if>
         <xsl:apply-templates select="*[2]"/>
        </m:mfenced>
@@ -1815,7 +1923,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[2]"/>
         <m:mo mathcolor="Green">
          <xsl:if test="$id != ''">
-          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
          </xsl:if>&#8773;</m:mo>
         <xsl:apply-templates select="*[3]"/>
       </xsl:when>
@@ -1823,7 +1931,7 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:when test="$name='forgetful'">
        <m:mfenced open="[" close="]">
         <xsl:if test="$id != ''">
-         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
         </xsl:if>
         <xsl:apply-templates select="*[2]"/>
        </m:mfenced>
@@ -1898,7 +2006,7 @@ which generates the toplevel element (see for instance xlink) -->
     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
     <m:mrow>
      <xsl:if test="@id">
-      <xsl:attribute name="m:xref">
+      <xsl:attribute name="xref">
        <xsl:value-of select="@id"/>
       </xsl:attribute>
      </xsl:if>