X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=0d23a1837ce3803999615b9cc12d8571b9af275f;hb=d7f8a683aebae3ec4932296659185f97b5882c23;hp=566ccdf0a131f5523545592cb2bbd7439db736f7;hpb=aa87f28d3a96456e7cec9493c6533e5c146812e8;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 566ccdf0a..0d23a1837 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1,5 +1,29 @@
 <?xml version="1.0"?>
 
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
 <!--***********************************************************************--> 
 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
@@ -18,7 +42,7 @@
 <!-- Parameter affecting line-breaking                                     -->
 <!--***********************************************************************-->
 
-<xsl:variable name="framewidth" select="30"/>
+<xsl:variable name="framewidth" select="35"/>
 
 <!--***********************************************************************-->
 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
@@ -295,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>
@@ -349,13 +390,86 @@
       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
+      <xsl:when test="$name='forall'">
+       <xsl:choose>
+       <xsl:when test="$charlength >= $framewidth">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+            <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
+            <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:mtable>
+       </xsl:when>
+       <xsl:otherwise>
+        <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"/>
+        <m:mo>.</m:mo>
+        <xsl:apply-templates select="*[position()=3]"/>
+       </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>
@@ -370,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"/>
@@ -394,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>
@@ -411,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>
@@ -474,7 +588,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="#b03060">:></m:mo>
+            <m:mo mathcolor="Maroon">:></m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -491,7 +605,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="#b03060">:></m:mo>
+        <m:mo mathcolor="Maroon">:></m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -560,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>
@@ -571,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>
@@ -601,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>
@@ -802,7 +916,8 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">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>
           </m:mtd>
@@ -877,7 +992,7 @@
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[3]"/>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>and apply</m:mtext>
+            <m:mtext>and apply to</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()>3]"/>
            </m:mrow>
@@ -913,6 +1028,7 @@
             <m:mtext>(</m:mtext>
             <xsl:apply-templates select="*[3]"/>
             <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[4]"/>
             </m:mrow>
           </m:mtd>
@@ -923,6 +1039,7 @@
             <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>
@@ -1012,6 +1129,8 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
           </m:mtd>
@@ -1028,6 +1147,8 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
           </m:mtd>
@@ -1048,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>
@@ -1063,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"/>
@@ -1214,9 +1335,9 @@
 <xsl:template match = "m:set">
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <m:mo> 
-    <m:mchar name="EmptySet"/>
-   </m:mo>
+   <m:mi> 
+    <m:mchar name="emptyset"/>
+   </m:mi>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="charlength">
@@ -1380,3 +1501,4 @@
 
 </xsl:stylesheet> 
 
+