X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=d0c8555b39ac48df5c4a91c1469350ffcff0dfdb;hb=5efc24038e24e64e39ec33d4c8f09e1fc6948366;hp=6572c0556c3f93890248c12c0fe70365fbbefaaf;hpb=5d9c64e007c6eff9447b2ef67d2a680c86c2775d;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6572c0556..d0c8555b3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -411,7 +411,7 @@ which generates the toplevel element (see for instance xlink) -->
     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
     <m:mrow>
-     <xsl:if test="@helm:xref">
+     <xsl:if test="@id">
       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
@@ -737,8 +737,8 @@ which generates the toplevel element (see for instance xlink) -->
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
-         <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
+         <xsl:for-each select="piecewise/piece">
+         <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
          <m:mtr>
           <m:mtd>
            <m:mrow>
@@ -751,10 +751,10 @@ which generates the toplevel element (see for instance xlink) -->
             </xsl:otherwise>
             </xsl:choose>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="."/>
+            <xsl:apply-templates select="./*[2]"/>
             <xsl:if test="$framewidth > $charlength">
              <m:mo mathcolor="Green">&#x21d2;</m:mo>
-             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+             <xsl:apply-templates select="./*[1]"/>
             </xsl:if>
            </m:mrow>
           </m:mtd>
@@ -765,7 +765,7 @@ which generates the toplevel element (see for instance xlink) -->
            <m:mrow>
             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
             <m:mo mathcolor="Green">&#x21d2;</m:mo>
-            <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+            <xsl:apply-templates select="./*[1]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -787,15 +787,15 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>OF</m:mo>
-        <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+        <xsl:for-each select="piecewise/piece">
          <xsl:choose>
          <xsl:when test="position() != 1">
           <m:mo stretchy="false">|</m:mo>
          </xsl:when> 
          </xsl:choose>
-         <xsl:apply-templates select="."/>
+         <xsl:apply-templates select="./*[2]"/>
          <m:mo mathcolor="Green">&#x21d2;</m:mo>
-         <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+         <xsl:apply-templates select="./*[1]"/>
         </xsl:for-each>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
         <m:mo>END</m:mo>
@@ -988,8 +988,12 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- PROOF -->
       <xsl:when test="$name='proof'">
        <m:maction actiontype="toggle">
-        <!-- CSC: next if until the annotationHelper can handle mactions -->
-        <xsl:if test="not($explodeall)">
+        <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
+        <xsl:variable name="test" select="(not($explodeall)) and
+	   (not(preceding-sibling::*[1]/text()='letin1')) and
+	   (not(preceding-sibling::*[1]/text()='rw_step')) and
+	   (not(name(..)='m:lambda'))"/>
+        <xsl:if test="$test">
          <!-- Details hided (default) -->
          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
           <m:mtr>
@@ -1026,7 +1030,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mphantom>
               <m:mtext>_</m:mtext>
              </m:mphantom>
-             <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
             </m:mrow>
            </m:mrow>
           </m:mtd>
@@ -1520,6 +1526,131 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- ***************************************** -->
+      <!-- *********** NOTATIONS ******************* -->
+      <!-- ***************************************** -->
+      <!-- subst -->
+      <xsl:when test="$name='subst'">
+        <xsl:apply-templates select="*[3]"/>
+<!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
+        <m:mo stretchy="false">[</m:mo>
+        <xsl:apply-templates select="*[4]"/>
+        <m:mo mathcolor="green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8592;</m:mo>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">]</m:mo>
+      </xsl:when>
+      <!-- lift -->
+      <xsl:when test="$name='lift'">
+        <m:msup>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[2]"/>
+        </m:msup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[3]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>
+      </xsl:when>
+      <!-- lift_with_base -->
+      <xsl:when test="$name='lift_with_base'">
+        <m:msubsup>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[3]"/>
+	 <xsl:apply-templates select="*[4]"/>
+        </m:msubsup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[2]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>	
+      </xsl:when>
+      <!-- beta_red1 -->
+      <xsl:when test="$name='beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- beta_red -->
+      <xsl:when test="$name='beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+          <m:mi mathcolor="green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red1 -->
+      <xsl:when test="$name='par_beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red -->
+      <xsl:when test="$name='par_beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+          <m:mi mathcolor="green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- forgetful -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="|" close="|">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when>
+      <!-- isomorphic -->
+      <xsl:when test="$name='isomorphic'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo mathcolor="green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8773;</m:mo>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- interp -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="[" close="]">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when> 
+
       <!-- ERROR -->
       <xsl:otherwise>
        <m:mi>ERROR</m:mi>
@@ -1587,7 +1718,12 @@ which generates the toplevel element (see for instance xlink) -->
 
 <xsl:template match="m:lambda">
     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
-    <m:mrow m:xref="{@id}">
+    <m:mrow>
+     <xsl:if test="@id">
+      <xsl:attribute name="m:xref">
+       <xsl:value-of select="@id"/>
+      </xsl:attribute>
+     </xsl:if>
      <xsl:choose>
      <xsl:when test="$charlength >= $framewidth">
       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1634,7 +1770,7 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:choose>
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
+    <xsl:if test="@id">
      <xsl:attribute name="m:xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
@@ -1652,7 +1788,12 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtd>
        <m:mrow>
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo m:xref="{m:in/@id}">=</m:mo>
+        <m:mo>
+         <xsl:if test="m:in/@id">
+          <xsl:attribute name="m:xref">
+           <xsl:value-of select="m:in/@id"/>
+          </xsl:attribute>
+         </xsl:if>=</m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1727,7 +1868,7 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:choose>
   <xsl:when test="$charlength >= $framewidth">
    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
-    <xsl:if test="@helm:xref">
+    <xsl:if test="@id">
      <xsl:attribute name="m:xref">
       <xsl:value-of select="@id"/>
      </xsl:attribute>
@@ -1745,7 +1886,12 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtd>
        <m:mrow>
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
+        <m:mo>
+         <xsl:if test="*[1]/@id">
+          <xsl:attribute name="m:xref">
+           <xsl:value-of select="*[1]/@id"/>
+          </xsl:attribute>
+         </xsl:if><xsl:value-of select="$symbol"/></m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1769,7 +1915,12 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:template match = "m:set">
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <m:mi>&#x02205;</m:mi>
+   <m:mi>
+    <xsl:if test="@id">
+     <xsl:attribute name="m:xref">
+      <xsl:value-of select="@id"/>
+     </xsl:attribute>
+    </xsl:if>&#x02205;</m:mi>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="charlength">
@@ -1783,7 +1934,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">{</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>{</m:mo>
            <xsl:apply-templates select="*[position()=1]"/>
           </m:mrow>
          </m:mtd>
@@ -1800,7 +1956,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">}</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>}</m:mo>
           </m:mrow>
          </m:mtd>
         </m:mtr>
@@ -1811,7 +1972,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">{</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>{</m:mo>
            <xsl:apply-templates select="*[position()=1]"/>
            <xsl:if test="position() != last()">
             <mo>,</mo>
@@ -1835,7 +2001,12 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mo stretchy="false">}</m:mo>
+           <m:mo stretchy="false">
+            <xsl:if test="@id">
+             <xsl:attribute name="m:xref">
+              <xsl:value-of select="@id"/>
+             </xsl:attribute>
+            </xsl:if>}</m:mo>
           </m:mrow>
          </m:mtd>
         </m:mtr>
@@ -1862,11 +2033,6 @@ which generates the toplevel element (see for instance xlink) -->
   </m:mfenced>
 </xsl:template>
 
-<!-- *********************************** -->
-<!--          PROOF ELEMENTS             -->
-<!-- *********************************** -->
-
-
 
 <!--**********************-->
 <!--       COUNTING       -->