Modified Files:

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index e130b4fb6aff8fceeaf5436ebcf3cb8410a61066..0d23a1837ce3803999615b9cc12d8571b9af275f 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -319,6 +319,23 @@
         </m:mrow>
        </m:mtd>
       </m:mtr>
+      <xsl:if test="name(*[1])='body'">
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mtext>AS</m:mtext>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+          <xsl:apply-templates select="body/*[1]"/>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+      </xsl:if>
      </m:mtable>
     </m:math>
 </xsl:template>
@@ -379,7 +396,7 @@
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+            <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -394,7 +411,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+        <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -403,13 +420,56 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <xsl:when test="$name='letin'">
+       <xsl:choose>
+       <xsl:when test="$charlength >= $framewidth">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+            <m:mo>LET</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="m:bvar"/>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>=</m:mo>
+            <xsl:apply-templates select="*[position()=3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>IN</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[position()=4]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:mo>LET</m:mo>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="m:bvar/m:ci"/>
+        <m:mo>=</m:mo>
+        <xsl:apply-templates select="*[position()=3]"/>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <m:mtext>IN</m:mtext>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="*[position()=4]"/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when> 
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue">&#x03a0;</m:mo>
+            <m:mo mathcolor="Blue">&#x03a0;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -424,7 +484,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue">&#x03a0;</m:mo>
+        <m:mo mathcolor="Blue">&#x03a0;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -448,7 +508,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Blue">&#x2192;</m:mo>
+            <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -465,7 +525,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Blue">&#x2192;</m:mo>
+        <m:mo mathcolor="Blue">&#x2192;</m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -528,7 +588,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Maroon">:></m:mo>
+            <m:mo mathcolor="Maroon">:></m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -545,7 +605,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Maroon">:></m:mo>
+        <m:mo mathcolor="Maroon">:></m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -614,7 +674,7 @@
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
             <xsl:if test="$framewidth > $charlength">
-             <m:mo color="Green">&#x21d2;</m:mo>
+             <m:mo mathcolor="Green">&#x21d2;</m:mo>
              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
             </xsl:if>
            </m:mrow>
@@ -625,7 +685,7 @@
           <m:mtd>
            <m:mrow>
             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
-            <m:mo color="Green">&#x21d2;</m:mo>
+            <m:mo mathcolor="Green">&#x21d2;</m:mo>
             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
            </m:mrow>
           </m:mtd>
@@ -655,7 +715,7 @@
          </xsl:when> 
          </xsl:choose>
          <xsl:apply-templates select="."/>
-         <m:mo color="Green">&#x21d2;</m:mo>
+         <m:mo mathcolor="Green">&#x21d2;</m:mo>
          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
         </xsl:for-each>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
@@ -856,7 +916,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we proved </m:mtext>
+            <m:mtext mathcolor="Maroon">we proved </m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
@@ -1069,7 +1129,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1087,7 +1147,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1109,7 +1169,7 @@
       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
           <m:mtd>
-            <m:mo color="Red">&#x03bb;</m:mo>
+            <m:mo mathcolor="Red">&#x03bb;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -1124,7 +1184,7 @@
       </m:mtable>
      </xsl:when>
      <xsl:otherwise>
-      <m:mo color="Red">&#x03bb;</m:mo>
+      <m:mo mathcolor="Red">&#x03bb;</m:mo>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <m:mo>:</m:mo>
       <xsl:apply-templates select="m:bvar/m:type"/>
@@ -1441,3 +1501,4 @@
 
 </xsl:stylesheet> 
 
+