]> matita.cs.unibo.it Git - helm.git/commitdiff
"Rewrite ... with ... by ..." line-breaking handled.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Dec 2002 18:49:15 +0000 (18:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Dec 2002 18:49:15 +0000 (18:49 +0000)
helm/style/mmlextension.xsl

index 377980f3f3bd6dd4b38eb1e9cd416cc50a3c0dd7..86d026562b4c1430c5e0c72892c15272304e97b5 100644 (file)
@@ -1537,23 +1537,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
@@ -2145,6 +2234,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">