]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/mmlextension.xsl
Minor bug fixes in the 'instantiate' element handling.
[helm.git] / helm / style / mmlextension.xsl
index c74bc4746cfdf5b3fca6f8499f3e60fbd282a359..1c19b50aabf763d780705edab11939dfc3904499 100644 (file)
@@ -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>