From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2002 11:05:59 +0000 (+0000)
Subject: 1) Sequent object added.
X-Git-Tag: V_0_3_0_debian_8~176
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e271d6d3bf82d56b6a72717759b5319dcf7c67f8;p=helm.git

1) Sequent object added.
2) Current Proof and META rendering improved.
---

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 95a1f66b2..ef9c297a6 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -169,7 +169,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <xsl:template match="META" mode="pure">
     <m:ci helm:xref="{@id}">
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@no"/></xsl:with-param></xsl:call-template>
+     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value">?<xsl:value-of select="@no"/></xsl:with-param></xsl:call-template>
     </m:ci>
 </xsl:template>
 
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index b9cd3165e..f92205008 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -183,7 +183,8 @@ 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>
+         <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:mrow>
        </m:mtd>
@@ -192,7 +193,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 +361,47 @@ which generates the toplevel element (see for instance xlink) -->
     </m:math>
 </xsl:template>
 
+<!-- SEQUENT -->
+
+<xsl:template match="Sequent">
+    <m:math>
+     <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
+      <xsl:for-each select="Declaration|Definition">
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mi><xsl:value-of select="@name"/></m:mi>
+          <xsl:choose>
+           <xsl:when test="name(.) = 'Declaration'">
+            <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>
+      <m:mtr>
+       <m:mtd>
+        <m:mrow>
+         <m:mtext>========================================</m:mtext>
+        </m:mrow>
+       </m:mtd>
+      </m:mtr>
+      <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         -->
 <!--**********************-->
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index 9b9825051..aef9daa6b 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -54,6 +54,22 @@
 
 <!-- CIC OBJECTS -->
 
+<xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
+    <Sequent helm:xref="{@id}">
+     <xsl:for-each select="Declaration|Definition">
+      <xsl:copy>
+       <xsl:attribute name="name">
+        <xsl:value-of select="@name"/>
+       </xsl:attribute>
+       <xsl:apply-templates select="*[1]"/>
+      </xsl:copy>
+     </xsl:for-each>
+     <Goal>
+      <xsl:apply-templates select="Goal/*[1]"/>
+     </Goal>
+    </Sequent> 
+</xsl:template>
+
 <xsl:template match="Definition" mode="noannot">
     <Definition name="{@name}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
@@ -98,7 +114,7 @@
 <xsl:template match="CurrentProof" mode="noannot">
     <CurrentProof name="{@name}" helm:xref="{@id}">
      <xsl:for-each select="Conjecture">
-      <Conjecture no="./{@no}">
+      <Conjecture no="{@no}">
         <xsl:apply-templates select="."/>
       </Conjecture>
      </xsl:for-each>