Explicit substitutions for metavariables introduced and DTD changed.

[helm.git] / helm / style / mmlextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index b9cd3165ef2bc2e4d1e98ed03d4fb4ce686950a6..7aeec143f15f8a2cf3b11cbb934ae7aa900fee91 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -183,8 +183,52 @@ which generates the toplevel element (see for instance xlink) -->
        <m:mtd>
         <m:mrow>
          <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>
+             <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: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>
+          <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         -->
 <!--**********************-->
@@ -418,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>