From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Dec 2002 17:15:21 +0000 (+0000)
Subject: Quick implementation of the "inst" csymbol. It can surely be improved.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0cc3da0c46191687bad5104b9947d311f1ad6918;p=helm.git

Quick implementation of the "inst" csymbol. It can surely be improved.
---

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 4a801a654..c74bc4746 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1105,6 +1105,26 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- INST -->
+      <xsl:when test="$name='inst'">
+       <m:mrow>
+        <xsl:if test="@definitionURL">
+         <xsl:attribute name="helm:xref" value="{@helm:xref}"/>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">{</m:mo>
+        <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+         <xsl:if test="name()='m:ci'">
+          <a href="{@definitionURL}">
+           <xsl:apply-templates/>
+          </a>
+         </xsl:if>
+         <m:mo stretchy="false">:=</m:mo>
+         <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+        </xsl:for-each>
+        <m:mo stretchy="false">}</m:mo>
+       </m:mrow>
+      </xsl:when>
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
@@ -1977,7 +1997,7 @@ which generates the toplevel element (see for instance xlink) -->
 
       <!-- ERROR -->
       <xsl:otherwise>
-       <m:mi>ERROR</m:mi>
+       <m:mi>ERROR(&quot;<xsl:value-of select="$name"/>&quot;)</m:mi>
       </xsl:otherwise>
      </xsl:choose>
     </m:mrow>