Sequent rendering improved: "=======" replaced by a single solid line

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index f92205008f00708b89415de1a5adb9c55ed34896..65a2b4612f01e90d00ffcadd01d3261bc50e3a81 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -364,8 +364,16 @@ which generates the toplevel element (see for instance xlink) -->
 <!-- SEQUENT -->
 
 <xsl:template match="Sequent">
+ <xsl:variable name="rowlines">
+  <xsl:for-each select="Declaration|Definition">
+   <xsl:if test="position() != last()">
+    <xsl:text>none </xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+  <xsl:text>solid</xsl:text>
+ </xsl:variable>
     <m:math>
-     <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
+     <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
       <xsl:for-each select="Declaration|Definition">
        <m:mtr>
         <m:mtd>
@@ -384,13 +392,15 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtd>
        </m:mtr>
       </xsl:for-each>
+      <xsl:if test="not(Declaration|Definition)">
       <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>