----------------------------------------------------------------------

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index bb13c876ebcd93bf38997b2c190d2a0b3e258747..6572c0556c3f93890248c12c0fe70365fbbefaaf 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -373,21 +373,27 @@ which generates the toplevel element (see for instance xlink) -->
      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
       <m:mtr>
        <m:mtd>
-        <xsl:apply-templates select="m:ci"/>
-        <m:mo>:</m:mo>
+        <m:mrow>
+         <xsl:apply-templates select="m:ci"/>
+         <m:mo>:</m:mo>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
       <m:mtr>
        <m:mtd>
+        <m:mrow>
          <xsl:apply-templates select="m:type"/>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
      </m:mtable>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:apply-templates select="m:ci"/>
-     <m:mo>:</m:mo>
-     <xsl:apply-templates select="m:type"/>
+     <m:mrow>
+      <xsl:apply-templates select="m:ci"/>
+      <m:mo>:</m:mo>
+      <xsl:apply-templates select="m:type"/>
+     </m:mrow>
     </xsl:otherwise>
    </xsl:choose>
   </xsl:when>
@@ -417,7 +423,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
+            <m:mo mathcolor="Blue">&#8704;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
            </m:mrow>
           </m:mtd>
@@ -433,7 +439,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
+        <m:mo mathcolor="Blue">&#8704;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -985,17 +991,21 @@ which generates the toplevel element (see for instance xlink) -->
         <!-- CSC: next if until the annotationHelper can handle mactions -->
         <xsl:if test="not($explodeall)">
          <!-- Details hided (default) -->
-         <m:mrow>
-          <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
-          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-          <xsl:apply-templates select="*[position()=3]"/>
-          <m:mrow>
-           <m:mphantom>
-            <m:mtext>_</m:mtext>
-           </m:mphantom>
-           <m:mtext mathcolor="Green">(explain)</m:mtext>
-          </m:mrow>
-         </m:mrow>
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <xsl:apply-templates select="*[position()=3]"/>
+             <m:mrow>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <m:mtext mathcolor="Green">(explain)</m:mtext>
+             </m:mrow>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
         </xsl:if>
         <!-- Show details -->
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1009,7 +1019,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we&#x00a0;proved </m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
             <m:mrow>
@@ -1043,15 +1053,12 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-
-      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
-      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
       <xsl:when test="$name='by_induction'">
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">We prove </m:mtext>
+           <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <xsl:apply-templates select="../*[3]"/>
           </m:mrow>
@@ -1060,9 +1067,9 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">by induction on </m:mtext>
+           <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates
+           <xsl:apply-templates 
             select="*[position()=last()]/*[position()=last()]"/>
           </m:mrow>
          </m:mtd>
@@ -1070,12 +1077,13 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
             <xsl:for-each select="*[position()>3 and not(position()=last())]">
              <m:mtr>
               <m:mtd>
-               <xsl:apply-templates select="."/>
+               <m:mrow>
+                <xsl:apply-templates select="."/>
+               </m:mrow>
               </m:mtd>
              </m:mtr>
             </xsl:for-each>
@@ -1091,7 +1099,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">Case </m:mtext>
+           <m:mtext mathcolor="red">Case</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <xsl:apply-templates select="*[2]"/>
           </m:mrow>
@@ -1105,7 +1113,9 @@ which generates the toplevel element (see for instance xlink) -->
             <xsl:if test="*[3]/*[position()>1]">
              <m:mtr>
               <m:mtd>
-               <m:mtext mathcolor="red">By induction hypothesis, we have:</m:mtext>
+               <m:mrow>
+                <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
+               </m:mrow>
               </m:mtd>
              </m:mtr>
              <m:mtr>
@@ -1125,7 +1135,9 @@ which generates the toplevel element (see for instance xlink) -->
             </xsl:if>
             <m:mtr>
              <m:mtd>
-              <xsl:apply-templates select="*[4]"/>
+              <m:mrow>
+               <xsl:apply-templates select="*[4]"/>
+              </m:mrow>
              </m:mtd>
             </m:mtr>
            </m:mtable>
@@ -1155,6 +1167,7 @@ which generates the toplevel element (see for instance xlink) -->
         </xsl:choose>
        </m:mrow>
       </xsl:when>
+      <!-- false_ind  -->
       <xsl:when test="$name='false_ind'">
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
@@ -1173,8 +1186,6 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtr>
        </m:mtable>
       </xsl:when>
-      <!--CSC fine della parte da risistemare -->
-
       <!-- LET-IN -->
       <xsl:when test="$name='letin'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1278,7 +1289,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Then apply it to</m:mtext>
+            <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()>2]"/>
            </m:mrow>
@@ -1308,7 +1319,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>In particular, we have</m:mtext>
+            <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -1343,8 +1354,6 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
-      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
       <!-- full_or_ind -->
       <xsl:when test="$name='full_or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1367,7 +1376,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>We proceed by cases to prove</m:mtext>
+            <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[3]"/>
            </m:mrow>
@@ -1376,7 +1385,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Left: suppose</m:mtext>
+            <m:mtext>Left:&#x00a0;suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mo stretchy="false">(</m:mo>
             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
@@ -1388,8 +1397,8 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <m:mrow>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[4]/*[3]"/>
            </m:mrow>
           </m:mtd>
@@ -1397,7 +1406,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Right: suppose</m:mtext>
+            <m:mtext>Right:&#x00a0;suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mo stretchy="false">(</m:mo>
             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
@@ -1416,7 +1425,6 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-      <!--CSC fine della parte da risistemare -->
       <!-- OR_IND -->
       <xsl:when test="$name='or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1439,11 +1447,11 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>We prove</m:mtext>
+            <m:mtext>We&#x00a0;prove</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>by cases:</m:mtext>
+            <m:mtext>by&#x00a0;cases:</m:mtext>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -1493,7 +1501,7 @@ which generates the toplevel element (see for instance xlink) -->
             <m:mtext>:</m:mtext>
             <xsl:apply-templates select="*[4]"/>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>such that</m:mtext>
+            <m:mtext>such&#x00a0;that</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mtext>(</m:mtext>
              <xsl:apply-templates select="*[5]"/>
@@ -1545,7 +1553,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1563,7 +1571,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1673,43 +1681,43 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:variable name="symbol">
   <xsl:choose>
    <xsl:when test="m:and[1]">
-    <xsl:value-of select="'wedge'"/>
+    <xsl:value-of select="'&#8743;'"/>
    </xsl:when>
    <xsl:when test="m:or[1]">
-    <xsl:value-of select="'vee'"/>
+    <xsl:value-of select="'&#8744;'"/>
    </xsl:when>
    <xsl:when test="m:geq[1]">
-    <xsl:value-of select="'geq'"/>
+    <xsl:value-of select="'&#8805;'"/>
    </xsl:when>
    <xsl:when test="m:leq[1]">
-    <xsl:value-of select="'leq'"/>
+    <xsl:value-of select="'&#8804;'"/>
    </xsl:when>
    <xsl:when test="m:gt[1]">
-    <xsl:value-of select="'gt'"/>
+    <xsl:value-of select="'&#62;'"/>
    </xsl:when>
    <xsl:when test="m:lt[1]">
-    <xsl:value-of select="'lt'"/>
+    <xsl:value-of select="'&#60;&#32;'"/>
    </xsl:when>
    <xsl:when test="m:eq[1]">
-    <xsl:value-of select="'Equal'"/>
+    <xsl:value-of select="'&#61;'"/>
    </xsl:when>
    <xsl:when test="m:in[1]">
-    <xsl:value-of select="'Element'"/>
+    <xsl:value-of select="'&#x02208;'"/>
    </xsl:when>
    <xsl:when test="m:subset[1]">
-    <xsl:value-of select="'SubsetEqual'"/>
+    <xsl:value-of select="'&#x02286;'"/>
    </xsl:when>
    <xsl:when test="m:prsubset[1]">
-    <xsl:value-of select="'subset'"/>
+    <xsl:value-of select="'&#x02282;'"/>
    </xsl:when>
    <xsl:when test="m:intersect[1]">
-    <xsl:value-of select="'Intersection'"/>
+    <xsl:value-of select="'&#x022C2;'"/>
    </xsl:when>
    <xsl:when test="m:union[1]">
-    <xsl:value-of select="'Union'"/>
+    <xsl:value-of select="'&#x022C3;'"/>
    </xsl:when>
    <xsl:when test="m:setdiff[1]">
-    <xsl:value-of select="'Backslash'"/>
+    <xsl:value-of select="'&#x02216;'"/>
    </xsl:when>
   </xsl:choose>
  </xsl:variable>
@@ -1737,9 +1745,7 @@ 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}"> 
-         <m:mchar name="{$symbol}"/>
-        </m:mo>
+        <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1763,9 +1769,7 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:template match = "m:set">
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <m:mi> 
-    <m:mchar name="emptyset"/>
-   </m:mi>
+   <m:mi>&#x02205;</m:mi>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="charlength">
@@ -1945,6 +1949,3 @@ which generates the toplevel element (see for instance xlink) -->
 </xsl:template>
 
 </xsl:stylesheet> 
-
-
-