From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Dec 2002 13:35:19 +0000 (+0000)
Subject: Minor bug fixes in the 'instantiate' element handling.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b58d7cd51389115f74edb883912178c866e00103;p=helm.git

Minor bug fixes in the 'instantiate' element handling.
---

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index e47126138..f2f7b713a 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -324,7 +324,10 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 </xsl:template>
 
 <xsl:template match="instantiate" mode="pure">
-	<m:apply helm:xref="{@id}">
+	<m:apply>
+         <xsl:if test="@id">
+          <xsl:attribute name="helm:xref" select="@id"/>
+         </xsl:if>
 	 <m:csymbol>inst</m:csymbol>
 	 <xsl:apply-templates mode="noannot" select="*[1]" />
 	 <xsl:for-each select="arg">
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index c74bc4746..1c19b50aa 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1108,17 +1108,13 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- INST -->
       <xsl:when test="$name='inst'">
        <m:mrow>
-        <xsl:if test="@definitionURL">
-         <xsl:attribute name="helm:xref" value="{@helm:xref}"/>
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
         </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>
+         <xsl:apply-templates/>
          <m:mo stretchy="false">:=</m:mo>
          <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
         </xsl:for-each>