Branch V7_3_new_exportation merged.

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 4a801a65402c244e03bbe273c6a4d7a7ba1709a3..fad3dce6b333edad5e4b32d06e5baa38c34cca9d 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1105,6 +1105,96 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- INST -->
+      <xsl:when test="$name='inst'">
+       <m:mrow>
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">{</m:mo>
+        <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+         <xsl:apply-templates select="."/>
+         <m:mo stretchy="false">:=</m:mo>
+         <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+        </xsl:for-each>
+        <m:mo stretchy="false">}</m:mo>
+       </m:mrow>
+      </xsl:when>
+      <!-- APPEND -->
+      <xsl:when test="$name='append'">
+       <xsl:choose>
+        <xsl:when test="$charlength >= $framewidth">
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[2]"/>
+             <m:mo>@</m:mo>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[3]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:mrow>
+          <xsl:apply-templates select="*[2]"/>
+          <m:mo>@</m:mo>
+          <xsl:apply-templates select="*[3]"/>
+         </m:mrow>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <!-- ITE -->
+      <xsl:when test="$name='ite'">
+       <xsl:choose>
+        <xsl:when test="$charlength >= $framewidth">
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>if</m:mo>
+             <xsl:apply-templates select="*[2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>then</m:mo>
+             <xsl:apply-templates select="*[3]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>else</m:mo>
+             <xsl:apply-templates select="*[4]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:mrow>
+          <m:mo>if</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+          <m:mo>then</m:mo>
+          <xsl:apply-templates select="*[3]"/>
+          <m:mo>else</m:mo>
+          <xsl:apply-templates select="*[4]"/>
+         </m:mrow>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
@@ -1478,23 +1568,112 @@ which generates the toplevel element (see for instance xlink) -->
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <m:mtr>
-          <m:mtd>
-           <m:mrow>
-            <m:mtext>Rewrite</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[3]"/>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <m:mtext>with</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[4]"/>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>by</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[5]"/>
-           </m:mrow>
-          </m:mtd>
-         </m:mtr>
+         <xsl:variable name="charlength1">
+          <xsl:apply-templates select="*[3]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="charlength2">
+          <xsl:apply-templates select="*[4]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="charlength3">
+          <xsl:apply-templates select="*[5]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="split1"
+           select="($charlength1 + $charlength2) >= $framewidth"/>
+         <xsl:variable name="split2"
+           select="($charlength2 + $charlength3) >= $framewidth"/>
+         <xsl:choose>
+          <xsl:when test="$split1">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+           <xsl:choose>
+            <xsl:when test="$split2">
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+               <m:mtext>with</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[4]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <m:mtext>by</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[5]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:when>
+            <xsl:otherwise>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+               <m:mtext>with</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[4]"/>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <m:mtext>by</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[5]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:otherwise>
+           </xsl:choose>
+          </xsl:when>
+          <xsl:when test="$split2">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <m:mtext>with</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[4]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>by</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[5]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:when>
+          <xsl:otherwise>
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <m:mtext>with</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[4]"/>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <m:mtext>by</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[5]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:otherwise>
+         </xsl:choose>
         </m:mtable>
       </xsl:when>
       <!-- not existing any more
@@ -1966,7 +2145,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[3]"/>
       </xsl:when>
       <!-- interp -->
-      <xsl:when test="$name='forgetful'">
+      <xsl:when test="$name='interp'">
        <m:mfenced open="[" close="]">
         <xsl:if test="$id != ''">
          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
@@ -1977,7 +2156,7 @@ which generates the toplevel element (see for instance xlink) -->
 
       <!-- ERROR -->
       <xsl:otherwise>
-       <m:mi>ERROR</m:mi>
+       <m:mi>ERROR(&quot;<xsl:value-of select="$name"/>&quot;)</m:mi>
       </xsl:otherwise>
      </xsl:choose>
     </m:mrow>
@@ -2086,6 +2265,24 @@ which generates the toplevel element (see for instance xlink) -->
 <!--       COUNTING       -->
 <!--**********************-->
 
+<!-- enter this counting mode selecting the root -->
+<xsl:template match="*" mode="root_charcount">
+<xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+  <xsl:when test="count(*)=0">
+   <xsl:value-of select="0"/>
+  </xsl:when>
+  <xsl:when test="name()='m:ci'">
+   <xsl:value-of select="string-length()"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates select="*[1]" mode="charcount">
+    <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
+   </xsl:apply-templates>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
  |m:plus|m:minus|m:times" mode="charcount">
@@ -2113,14 +2310,24 @@ which generates the toplevel element (see for instance xlink) -->
 </xsl:template>
 
 <xsl:template match="m:ci|m:csymbol" mode="charcount">
-<xsl:param name="incurrent_length" select="0"/> 
-<xsl:param name="nosibling" select="0"/>
+ <xsl:param name="incurrent_length" select="0"/> 
+ <xsl:param name="nosibling" select="0"/>
+ <xsl:variable name="mylength">
+  <xsl:choose>
+   <!-- special notation -->
+   <xsl:when test="text()='append'">3</xsl:when>
+   <!-- no notation -->
+   <xsl:otherwise>
+    <xsl:value-of select="string-length()"/>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:variable>
     <xsl:choose>
-    <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
-     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+    <xsl:when test="$framewidth > ($incurrent_length + $mylength) and ($nosibling = 0)">
+     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + $mylength"/></xsl:apply-templates></xsl:variable>
      <xsl:choose>
      <xsl:when test="string($siblength) = &quot;&quot;">
-      <xsl:value-of select="$incurrent_length + string-length()"/>
+      <xsl:value-of select="$incurrent_length + $mylength"/>
      </xsl:when>
      <xsl:otherwise>
       <xsl:value-of select="number($siblength)"/>
@@ -2128,7 +2335,7 @@ which generates the toplevel element (see for instance xlink) -->
      </xsl:choose>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:value-of select="$incurrent_length + string-length()"/>
+     <xsl:value-of select="$incurrent_length + $mylength"/>
     </xsl:otherwise>
     </xsl:choose>
 </xsl:template>