Modified Files:

[helm.git] / helm / style / mmlextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 67859db656d243d62babbc0a06ecc6dea80cf792..5a9a391d3466dd130f83df6d76ae72e26e304e34 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -32,11 +32,16 @@
 <!-- Revised: March 21 2000, Irene Schena                                  -->
 <!--***********************************************************************--> 
 
+<!-- NOTE: the namespace declaration has to be done in the stylesheets 
+which generates the toplevel element (see for instance xlink) -->
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
-                              xmlns:helm="http://www.cs.unibo.it/helm">
+                              xmlns:helm="http://www.cs.unibo.it/helm"
+                              xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
+<xsl:import href="mmlctop.xsl-0.14"/>
 
-<xsl:import href="mml2mmlv1_0.xsl"/>
 <xsl:import href="mmltheoryextension.xsl"/>
 
 <!--***********************************************************************-->
@@ -391,7 +396,7 @@
     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
     <m:mrow>
      <xsl:if test="@helm:xref">
-      <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
+      <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
       <xsl:when test="$name='forall'">
@@ -400,8 +405,10 @@
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
+           <m:mrow>
             <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -430,9 +437,11 @@
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
+           <m:mrow>
             <m:mo>LET</m:mo>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -473,8 +482,10 @@
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
+           <m:mrow>
             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -1138,7 +1149,9 @@
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mtext>In particular, we have</m:mtext>
+           <m:mrow>
+            <m:mtext>In particular, we have</m:mtext>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -1192,11 +1205,13 @@
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mtext>We prove</m:mtext>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates select="*[3]"/>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <m:mtext>by cases:</m:mtext>
+           <m:mrow>
+            <m:mtext>We prove</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>by cases:</m:mtext>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -1237,19 +1252,21 @@
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mtext>Let</m:mtext>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates select="*[3]"/>
-           <m:mtext>:</m:mtext>
-           <xsl:apply-templates select="*[4]"/>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <m:mtext>such that</m:mtext>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <m:mtext>(</m:mtext>
-            <xsl:apply-templates select="*[5]"/>
-           <m:mtext>)</m:mtext>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates select="*[6]"/>
+           <m:mrow>
+            <m:mtext>Let</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
+            <m:mtext>:</m:mtext>
+            <xsl:apply-templates select="*[4]"/>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>such that</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <m:mtext>(</m:mtext>
+             <xsl:apply-templates select="*[5]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[6]"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
@@ -1327,14 +1344,16 @@
 
 <xsl:template match="m:lambda">
     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
-    <m:mrow helm:xref="{@helm:xref}">
+    <m:mrow m:xref="{@id}">
      <xsl:choose>
      <xsl:when test="$charlength >= $framewidth">
       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
           <m:mtd>
+           <m:mrow>
             <m:mo mathcolor="Red">&#x03bb;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
        <m:mtr>
@@ -1373,28 +1392,34 @@
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
     <xsl:if test="@helm:xref">
-     <xsl:attribute name="helm:xref">
-      <xsl:value-of select="@helm:xref"/>
+     <xsl:attribute name="m:xref">
+      <xsl:value-of select="@id"/>
      </xsl:attribute>
     </xsl:if>    
     <m:mtr>
      <m:mtd>
-      <m:mo stretchy="false">(</m:mo>
-      <xsl:apply-templates select="*[position()=2]"/>
+      <m:mrow>
+       <m:mo stretchy="false">(</m:mo>
+       <xsl:apply-templates select="*[position()=2]"/>
+      </m:mrow>
      </m:mtd>
     </m:mtr>
     <xsl:for-each select = "*[position()>2]">
      <m:mtr>
       <m:mtd>
-       <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
-       <xsl:apply-templates select="."/>
+       <m:mrow>
+        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+        <m:mo m:xref="{m:in/@id}">=</m:mo>
+        <xsl:apply-templates select="."/>
+       </m:mrow>
       </m:mtd>
      </m:mtr>
     </xsl:for-each>
     <m:mtr>
      <m:mtd>
-      <m:mo stretchy="false">)</m:mo>
+      <m:mrow>
+       <m:mo stretchy="false">)</m:mo>
+      </m:mrow>
      </m:mtd>
     </m:mtr>
    </m:mtable>
@@ -1460,30 +1485,36 @@
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
     <xsl:if test="@helm:xref">
-     <xsl:attribute name="helm:xref">
-      <xsl:value-of select="@helm:xref"/>
+     <xsl:attribute name="m:xref">
+      <xsl:value-of select="@id"/>
      </xsl:attribute>
     </xsl:if>    
     <m:mtr>
      <m:mtd>
-      <m:mo stretchy="false">(</m:mo>
-      <xsl:apply-templates select="*[position()=2]"/>
+      <m:mrow>
+       <m:mo stretchy="false">(</m:mo>
+       <xsl:apply-templates select="*[position()=2]"/>
+      </m:mrow>
      </m:mtd>
     </m:mtr>
     <xsl:for-each select = "*[position()>2]">
      <m:mtr>
       <m:mtd>
-       <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="{*[1]/@helm:xref}"> 
-        <m:mchar name="{$symbol}"/>
-       </m:mo>
-       <xsl:apply-templates select="."/>
+       <m:mrow>
+        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+        <m:mo m:xref="{*[1]/@id}"> 
+         <m:mchar name="{$symbol}"/>
+        </m:mo>
+        <xsl:apply-templates select="."/>
+       </m:mrow>
       </m:mtd>
      </m:mtr>
     </xsl:for-each>
     <m:mtr>
      <m:mtd>
-      <m:mo stretchy="false">)</m:mo>
+      <m:mrow>
+       <m:mo stretchy="false">)</m:mo>
+      </m:mrow>
      </m:mtd>
     </m:mtr>
    </m:mtable>
@@ -1512,20 +1543,26 @@
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
          <m:mtd>
-          <m:mo stretchy="false">{</m:mo>
-          <xsl:apply-templates select="*[position()=1]"/>
+          <m:mrow>
+           <m:mo stretchy="false">{</m:mo>
+           <xsl:apply-templates select="*[position()=1]"/>
+          </m:mrow>
          </m:mtd>
         </m:mtr>
         <m:mtr>
          <m:mtd>
-          <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
-          <m:mo stretchy="false">|</m:mo>
-          <xsl:apply-templates select="m:condition/*[1]"/>
+          <m:mrow>
+           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
+           <m:mo stretchy="false">|</m:mo>
+           <xsl:apply-templates select="m:condition/*[1]"/>
+          </m:mrow>
          </m:mtd>
         </m:mtr>
         <m:mtr>
          <m:mtd>
-          <m:mo stretchy="false">}</m:mo>
+          <m:mrow>
+           <m:mo stretchy="false">}</m:mo>
+          </m:mrow>
          </m:mtd>
         </m:mtr>
        </m:mtable>
@@ -1534,27 +1571,33 @@
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
          <m:mtd>
-          <m:mo stretchy="false">{</m:mo>
-          <xsl:apply-templates select="*[position()=1]"/>
-          <xsl:if test="position() != last()">
-           <mo>,</mo>
-          </xsl:if>
+          <m:mrow>
+           <m:mo stretchy="false">{</m:mo>
+           <xsl:apply-templates select="*[position()=1]"/>
+           <xsl:if test="position() != last()">
+            <mo>,</mo>
+           </xsl:if>
+          </m:mrow>
          </m:mtd>
         </m:mtr>
         <xsl:for-each select = "*[position()>2]">
          <m:mtr>
           <m:mtd>
-           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
-           <xsl:apply-templates select="."/>
-           <xsl:if test="position() != last()">
-            <mo>,</mo>
-           </xsl:if>
+           <m:mrow>
+            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
+            <xsl:apply-templates select="."/>
+            <xsl:if test="position() != last()">
+             <mo>,</mo>
+            </xsl:if>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
         </xsl:for-each>
         <m:mtr>
          <m:mtd>
-          <m:mo stretchy="false">}</m:mo>
+          <m:mrow>
+           <m:mo stretchy="false">}</m:mo>
+          </m:mrow>
          </m:mtd>
         </m:mtr>
        </m:mtable>
@@ -1570,9 +1613,14 @@
 </xsl:template>      
 
 <xsl:template match = "m:apply[m:card[1]]">
- <m:mo stretchy="false">|</m:mo>
+  <m:mfenced open="|" close="|" stretchy="false">
+    <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
+      <xsl:attribute name="m:xref">
+        <xsl:value-of select="@id"/>
+      </xsl:attribute>
+    </xsl:if>
   <xsl:apply-templates select="*[2]"/>
- <m:mo stretchy="false">|</m:mo>
+  </m:mfenced>
 </xsl:template>
 
 <!-- *********************************** -->