From: Irene Schena <irene.schena@unibo.it>
Date: Fri, 27 Jul 2001 09:58:57 +0000 (+0000)
Subject: ----------------------------------------------------------------------
X-Git-Tag: v0_1_3~97
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6c462476daa856b7261dbb33734bda1c4846b66;p=helm.git

----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: m:xref fixed
----------------------------------------------------------------------
---

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 71a424d8b..c33176a71 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -411,7 +411,7 @@ which generates the toplevel element (see for instance xlink) -->
     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
     <m:mrow>
-     <xsl:if test="@helm:xref">
+     <xsl:if test="@id">
       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
@@ -1526,19 +1526,15 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- subst -->
       <xsl:when test="$name='subst'">
         <xsl:apply-templates select="*[3]"/>
-        <m:mo>&#xe8a0;</m:mo>
-        <m:mrow>
-         <m:mo stretchy="false">[</m:mo>
-         <m:mrow>
-          <xsl:apply-templates select="*[4]"/>
-          <m:mo mathcolor="green">
-           <xsl:if test="$id != ''">
-            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
-           </xsl:if>&#8592;</m:mo>
-          <xsl:apply-templates select="*[2]"/>
-         </m:mrow>
-         <m:mo stretchy="false">]</m:mo>
-        </m:mrow>
+<!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
+        <m:mo stretchy="false">[</m:mo>
+        <xsl:apply-templates select="*[4]"/>
+        <m:mo mathcolor="green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8592;</m:mo>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">]</m:mo>
       </xsl:when>
       <!-- lift -->
       <xsl:when test="$name='lift'">
@@ -1763,7 +1759,7 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:choose>
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
+    <xsl:if test="@id">
      <xsl:attribute name="m:xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
@@ -1781,7 +1777,12 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtd>
        <m:mrow>
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo m:xref="{m:in/@id}">=</m:mo>
+        <m:mo>
+         <xsl:if test="m:in/@id">
+          <xsl:attribute name="m:xref">
+           <xsl:value-of select="m:in/@id"/>
+          </xsl:attribute>
+         </xsl:if>=</m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1856,7 +1857,7 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:choose>
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
+    <xsl:if test="@id">
      <xsl:attribute name="m:xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
@@ -1874,7 +1875,12 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtd>
        <m:mrow>
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
+        <m:mo>
+         <xsl:if test="*[1]/@id">
+          <xsl:attribute name="m:xref">
+           <xsl:value-of select="*[1]/@id"/>
+          </xsl:attribute>
+         </xsl:if><xsl:value-of select="$symbol"/></m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1898,7 +1904,12 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:template match = "m:set">
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <m:mi>&#x02205;</m:mi>
+   <m:mi>
+    <xsl:if test="@id">
+     <xsl:attribute name="m:xref">
+      <xsl:value-of select="@id"/>
+     </xsl:attribute>
+    </xsl:if>&#x02205;</m:mi>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="charlength">
@@ -1912,7 +1923,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">{</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>{</m:mo>
            <xsl:apply-templates select="*[position()=1]"/>
           </m:mrow>
          </m:mtd>
@@ -1929,7 +1945,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">}</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>}</m:mo>
           </m:mrow>
          </m:mtd>
         </m:mtr>
@@ -1940,7 +1961,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">{</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>{</m:mo>
            <xsl:apply-templates select="*[position()=1]"/>
            <xsl:if test="position() != last()">
             <mo>,</mo>
@@ -1964,7 +1990,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">}</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>}</m:mo>
           </m:mrow>
          </m:mtd>
         </m:mtr>
@@ -1991,11 +2022,6 @@ which generates the toplevel element (see for instance xlink) -->
   </m:mfenced>
 </xsl:template>
 
-<!-- *********************************** -->
-<!--          PROOF ELEMENTS             -->
-<!-- *********************************** -->
-
-
 
 <!--**********************-->
 <!--       COUNTING       -->