X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fstyle%2Fmmlextension.xsl;h=698e8fce5f9a427cd5d22033960e8370e32447e6;hb=4055cb3c14899802b74d22d078e9edce0b7f3fbf;hp=87e31e8aede6e02d8e4e8e803a25bac13cf9ec55;hpb=22344b1810548a3a75e0a7f36d23e8f8117ff633;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 87e31e8ae..698e8fce5 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -18,7 +18,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-->
@@ -349,6 +349,36 @@
       <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 color="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 color="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='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -474,7 +504,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="#b03060">:></m:mo>
+            <m:mo color="Maroon">:></m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -491,7 +521,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="#b03060">:></m:mo>
+        <m:mo color="Maroon">:></m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -802,7 +832,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">we proved </m:mtext>
+            <m:mtext color="Maroon">we proved </m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
@@ -878,7 +908,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>
@@ -1015,7 +1045,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">we get</m:mtext>
+            <m:mtext color="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1033,7 +1063,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="#b03060">we get</m:mtext>
+            <m:mtext color="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1221,9 +1251,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">