]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/content_to_html.xsl
Notation for if then else.
[helm.git] / helm / style / content_to_html.xsl
index 21b663942dfd10528de197b42ef9dfca984a688b..1a66b86dd489cf8280e0d4a870afcf4abdec3717 100644 (file)
 
 <xsl:template name="make_indent">
  <xsl:param name="current_indent" select="0"/>
+ <!-- non funziona bene con netscape !!! 
+ <span>
+  <xsl:attribute name="style">
+   <xsl:value-of select="concat('margin-left:',string($current_indent div 3), 'em')"/>
+  </xsl:attribute>
+ </span> -->
   <xsl:if test="$current_indent > 0">
    <xsl:text>&#x00a0;</xsl:text>
    <xsl:call-template name="make_indent">
       </xsl:choose>
      </xsl:for-each>
     </xsl:when>
+    <!-- if then else -->
+    <xsl:when test="$name='ite'">
+     <xsl:text>if </xsl:text> 
+     <xsl:apply-templates select="*[2]"/>
+     <xsl:text> then </xsl:text>
+     <xsl:apply-templates select="*[3]"/>
+     <xsl:text> else </xsl:text>
+     <xsl:apply-templates select="*[4]"/>
+    </xsl:when>
     <!-- proof and side_proof -->
     <xsl:when test="$name='proof' or $name='side_proof'">
        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
         <xsl:with-param name="current_indent" select="$current_indent+5"/>
        </xsl:apply-templates>
       </xsl:when>
+      <!-- it then else -->
+      <xsl:when test="$name='ite'">
+       <xsl:text>if </xsl:text> 
+       <xsl:apply-templates select="*[2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates> 
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> then </xsl:text>
+       <xsl:apply-templates select="*[3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/>
+       </xsl:apply-templates>
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> else </xsl:text>
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/> 
+       </xsl:apply-templates>
+      </xsl:when>
 
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->