From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2002 12:37:18 +0000 (+0000)
Subject: Sequent rendering improved: "=======" replaced by a single solid line
X-Git-Tag: V_0_3_0_debian_8~175
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=564808f227d45537df5061e05d81fcc70cb06f9d;p=helm.git

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index f92205008..65a2b4612 100644
--- 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>