X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=a22dc0dd332d56fcc2c4fcf3ee480792d3017c03;hb=4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf;hp=87e31e8aede6e02d8e4e8e803a25bac13cf9ec55;hpb=22344b1810548a3a75e0a7f36d23e8f8117ff633;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 87e31e8ae..a22dc0dd3 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='let_in'">
+       <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,7 @@
          <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>
@@ -878,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>
@@ -984,6 +1098,49 @@
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <xsl:when test="$name='ex_ind'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider </m:mtext>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
+          </m:mtd>
+         </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:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:apply-templates select="*[7]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+      </xsl:when>
       <xsl:otherwise>
        <m:ci>ERROR</m:ci>
       </xsl:otherwise>
@@ -1015,7 +1172,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">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>
@@ -1033,7 +1190,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">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>
@@ -1055,7 +1212,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>
@@ -1070,7 +1227,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"/>
@@ -1109,9 +1266,7 @@
      <m:mtr>
       <m:mtd>
        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="m:in/@helm:xref"> 
-        =
-       </m:mo>
+       <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
        <xsl:apply-templates select="."/>
       </m:mtd>
      </m:mtr>
@@ -1221,9 +1376,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">
@@ -1387,3 +1542,4 @@
 
 </xsl:stylesheet> 
 
+