Notation for if then else.

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

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 31b8c766a42684d864835381075492cab4271ef0..8757d0023788c2233bad2756a498201c79c34513 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1121,6 +1121,49 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mo stretchy="false">}</m:mo>
        </m:mrow>
       </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 ************** -->
       <!-- ***************************************** -->