X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=fdf9b7829e3a5970d623ea95ca4f12ed23476849;hb=4668559563eede2f325545a100ff82b774085ed0;hp=b070e87fcfb03420ce8129c7380c96f32073c2cf;hpb=78f0e9834348f091eebe7904a97e9db0ec63825a;p=helm.git

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index b070e87fc..fdf9b7829 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -81,6 +81,30 @@
       <xsl:when test="$symbol = 'arrow'">
        <xsl:value-of select="'&#x00ae;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'RightArrow'">
+       <xsl:value-of select="'&#222;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'subst'">
+       <xsl:value-of select="'&#x00ac;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+       <xsl:value-of select="'&#x00ad;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+       <xsl:value-of select="'&#x00ae;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta'">
+       <xsl:value-of select="'&#x0062;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+       <xsl:value-of select="'&#x00de;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'isomorphic'">
+       <xsl:value-of select="'&#x0040;'"/>
+      </xsl:when>
+      <xsl:otherwise>
+       <xsl:text>???</xsl:text>
+      </xsl:otherwise>
      </xsl:choose>
     </xsl:variable>
     <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
@@ -102,6 +126,30 @@
       <xsl:when test="$symbol = 'arrow'">
        <xsl:value-of select="'&#8594;'"/>
       </xsl:when>
+      <xsl:when test="$symbol = 'RightArrow'">
+       <xsl:value-of select="'&#8658;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'subst'">
+       <xsl:value-of select="'&#8592;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+       <xsl:value-of select="'&#8593;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+       <xsl:value-of select="'&#8594;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'beta'">
+       <xsl:value-of select="'&#946;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+       <xsl:value-of select="'&#8658;'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'isomorphic'">
+       <xsl:value-of select="'&#8773;'"/>
+      </xsl:when>
+      <xsl:otherwise>
+       <xsl:text>???</xsl:text>
+      </xsl:otherwise>
      </xsl:choose>
     </xsl:variable>
     <FONT color="{$color}">
@@ -273,16 +321,21 @@
      <FONT color="red">CASE </FONT>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
      <FONT color="red"> OF </FONT>
-     <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+<xsl:for-each select="piecewise/piece">
+<!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
       <xsl:choose>
        <xsl:when test="not(position() = 1)">
         <xsl:text> | </xsl:text> 
        </xsl:when> 
       </xsl:choose>
-      <xsl:apply-templates mode="inline" select="."/>
-      <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
+<xsl:apply-templates mode="inline" select="./*[2]"/>
+      <xsl:call-template name="mksymbol-1">
+       <xsl:with-param name="symbol" select="'RightArrow'"/>
+       <xsl:with-param name="color" select="'green'"/>
+       <xsl:with-param name="size" select="'+0'"/>
+      </xsl:call-template>
       <xsl:apply-templates mode="inline"
-           select="following-sibling::*[position()= 1]"/>
+           select="./*[1]"/>
      </xsl:for-each>
     </xsl:when>
     <!-- FIX -->
@@ -364,9 +417,11 @@
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ac;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <xsl:text>]</xsl:text>
@@ -377,9 +432,11 @@
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
@@ -391,9 +448,11 @@
 
       <xsl:when test="$name='lift'">
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
@@ -407,13 +466,17 @@
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -422,13 +485,18 @@
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -437,13 +505,17 @@
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -452,13 +524,18 @@
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -477,9 +554,11 @@
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-        <FONT color="green" FACE="symbol">
-        <xsl:text>&#x0040;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
@@ -687,7 +766,8 @@
           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
          </xsl:apply-templates>
          <xsl:text> OF </xsl:text> 
-         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+         <xsl:for-each select="piecewise/piece">
+    <!--   <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
          <br/>
          <xsl:call-template name="make_indent">
           <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
@@ -700,11 +780,15 @@
              <xsl:text>| </xsl:text>
             </xsl:otherwise>
             </xsl:choose>
-            <xsl:apply-templates select="."/>
-            <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
+          <xsl:apply-templates select="./*[2]"/>
+            <xsl:call-template name="mksymbol-1">
+             <xsl:with-param name="symbol" select="'RightArrow'"/>
+             <xsl:with-param name="color" select="'green'"/>
+             <xsl:with-param name="size" select="'+0'"/>
+            </xsl:call-template>
             <xsl:variable name="body_size">
-             <xsl:apply-templates 
-              select="following-sibling::*[1]/*[1]" mode="charcount"/>
+  <xsl:apply-templates 
+              select="./*[1]/*[1]" mode="charcount"/>
             </xsl:variable>
             <xsl:choose>
              <xsl:when test="$body_size > $framewidth">
@@ -713,14 +797,14 @@
                <xsl:with-param name="current_indent" 
                     select="$current_indent + 8"/>   
               </xsl:call-template>
-	      <xsl:apply-templates 
-                   select="following-sibling::*[position()= 1]">
+<xsl:apply-templates 
+                   select="./*[1]">
               <xsl:with-param name="current_indent" 
                    select="$current_indent + 8"/>      
              </xsl:apply-templates>
             </xsl:when>
             <xsl:otherwise>
-             <xsl:apply-templates select="following-sibling::*[position()= 1]"
+     <xsl:apply-templates select="./*[1]"
                    mode="inline" />
             </xsl:otherwise>
            </xsl:choose>
@@ -1046,46 +1130,6 @@
         </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
-      <!-- nat_ind -->
-      <xsl:when test="$name='nat_ind_complete'">
-       <FONT color="red">By induction on&#x00a0;</FONT>
-       <xsl:apply-templates select="*[2]"/>:
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>0&#x00a0;</xsl:text>
-       <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>S(</xsl:text>
-       <xsl:apply-templates select="*[4]"/>
-       <xsl:text>)&#x00a0;</xsl:text>
-       <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
-       <FONT color="red">Assume by induction</FONT>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent +10"/> 
-       </xsl:call-template>
-       <xsl:text>(</xsl:text>
-       <xsl:apply-templates select="*[5]"/>
-       <xsl:text>)</xsl:text>
-       <xsl:apply-templates select="*[6]">
-        <xsl:with-param name="current_indent" select="$current_indent + 14"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent +10"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[7]">
-        <xsl:with-param name="current_indent" select="$current_indent + 10"/>
-       </xsl:apply-templates>
-      </xsl:when>
       <!-- false_ind -->
       <xsl:when test="$name='false_ind'">
        <xsl:apply-templates select="*[3]">
@@ -1223,7 +1267,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Left:&#x00a0;
        <xsl:apply-templates select="*[4]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -1231,7 +1275,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Right:&#x00a0;
        <xsl:apply-templates select="*[5]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -1286,9 +1330,11 @@
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="blue" SIZE="+0" FACE="symbol">
-        <xsl:text>&#x00ac;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'blue'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[2]"/>
        <xsl:text>]</xsl:text>
@@ -1299,9 +1345,11 @@
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
@@ -1313,9 +1361,11 @@
 
       <xsl:when test="$name='lift'">
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ad;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
@@ -1329,13 +1379,17 @@
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1344,13 +1398,18 @@
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00ae;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1359,13 +1418,17 @@
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1374,13 +1437,18 @@
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-       <FONT color="green" FACE="symbol">
-        <xsl:text>&#x00de;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        <SUB>
-        <FONT color="green" FACE="symbol">
-         <xsl:text>&#x0062;*</xsl:text>
-        </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="'beta'"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
+        <xsl:text>*</xsl:text>
        </SUB>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
@@ -1399,9 +1467,11 @@
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <a href="{*[1]/@definitionURL}">
-        <FONT color="green" FACE="symbol">
-        <xsl:text>&#x0040;</xsl:text>
-       </FONT>
+        <xsl:call-template name="mksymbol-1">
+         <xsl:with-param name="symbol" select="$name"/>
+         <xsl:with-param name="color" select="'green'"/>
+         <xsl:with-param name="size" select="'+0'"/>
+        </xsl:call-template>
        </a>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>