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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 4a801a65402c244e03bbe273c6a4d7a7ba1709a3..c74bc4746cfdf5b3fca6f8499f3e60fbd282a359 100644 (file)
--- 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>