X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=533cf22998ed1cceaa23e55e7f89644e601a0a00;hb=e1d232bab1b061d9098fd666ca24bed84b38f99e;hp=f2d6182740c34ff7796bdf57067c9e9dccfaccfe;hpb=975ab2f71a5e39379d44a494d73b8e05a8a0ad5d;p=helm.git

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index f2d618274..533cf2299 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -1,5 +1,29 @@
 <?xml version="1.0"?>
 
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:m="http://www.w3.org/1998/Math/MathML">
 
@@ -8,31 +32,54 @@
 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
 <!--***********************************************************************--> 
 
+<xsl:param name="getterURL" select="'http://localhost:8081/'"/>
+<xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
+<xsl:param name="keys" select="'C1,HC2'"/>
+<xsl:param name="naturalLanguage" select="'yes'"/>
+
+<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
+
+<xsl:variable name="header"><xsl:value-of select="$processorURL"/>apply?keys=<xsl:value-of select="$keys"/>&#x26;param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&#x26;param.keys=<xsl:value-of select="$keys"/>&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
 
 <xsl:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
 <xsl:include href="html_reals.xsl"/>
 
-
-<!-- <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>-->
-<xsl:variable name="header" select="document('http://localhost:8081/conf')/html_link"/>
-
 <xsl:variable name="showcast" select="0"/>
 
+<xsl:template name="makeURL">
+ <xsl:param name="url" select="''"/>
+ <xsl:value-of select="concat(string($header),string($url),'&#x26;param.CICURI=',string($url))"/>
+</xsl:template>
 
 <!--***********************************************************************-->
 <!-- HTML Head and Body                                                    -->
 <!--***********************************************************************-->
 
-<xsl:output method="html"/>
+<!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
+
+<!-- document needs method="xml" and searches locally for the dtd if        -->
+<!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
+<!-- For having output html must be media-type="html" and for having the    -->
+<!-- correct <br /> you must specify at least the remote dtd by means of    -->
+<!-- doctype-public                                                         -->
+<xsl:output 
+	method="xml" 
+	encoding="iso-8859-1" 
+	media-type="text/html"
+	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
 
 <xsl:variable name="framewidth" select="36"/>
 
 <xsl:template match="/">
  <xsl:param name="current_indent" select="0"/>
                <html> 
-                <head></head>
-                <body>
+                <head>
+                 <style>
+                 A { text-decoration: none }
+                 </style>
+                </head>
+                <body bgcolor="white">
                 <xsl:apply-templates>
                  <xsl:with-param name="current_indent" select="0"/>
                 </xsl:apply-templates>
@@ -47,7 +94,7 @@
 <xsl:template name="make_indent">
  <xsl:param name="current_indent" select="0"/>
   <xsl:if test="$current_indent > 0">
-   <xsl:text>&#x00A0;</xsl:text>
+   <xsl:text>&#x00a0;</xsl:text>
    <xsl:call-template name="make_indent">
     <xsl:with-param name="current_indent" select="$current_indent - 1"/> 
    </xsl:call-template>
@@ -55,7 +102,6 @@
 </xsl:template>
 
 <!-- Syntactic Sugar -->
-
 <xsl:template match="m:type">
 <xsl:param name="current_indent" select="0"/> 
 <xsl:apply-templates>
@@ -80,8 +126,194 @@
 </xsl:apply-templates>
 </xsl:template>
 
+<!--*********************************************************************-->
+<!--                         INLINE MODE                                 -->
+<!--*********************************************************************-->
+
+<!-- href -->
+<xsl:template mode="inline" match="m:ci">
+ <xsl:choose>
+  <xsl:when test="boolean(@definitionURL)">
+   <a>
+   <xsl:attribute name="href">
+    <xsl:call-template name="makeURL">
+     <xsl:with-param name="url" select="@definitionURL"/>
+    </xsl:call-template>
+   </xsl:attribute>
+   <xsl:apply-templates/>
+   </a>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="."/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
 <!-- CSYMBOL -->
 
+<xsl:template match="m:apply[m:csymbol]" mode="inline">
+   <xsl:variable name="name">
+    <xsl:value-of select="m:csymbol"/>
+   </xsl:variable>
+   <xsl:choose>
+    <!-- FORALL -->
+    <xsl:when test="$name='forall'">
+     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
+     <xsl:apply-templates select="m:bvar/m:ci"/>
+     <xsl:text>:</xsl:text>
+     <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+     <xsl:text>.</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+    </xsl:when>
+    <xsl:when test="$name='prod'">
+     <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
+     <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
+     <xsl:text>:</xsl:text>
+     <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+     <xsl:text>.</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+    </xsl:when>
+    <!-- ARROW -->
+    <xsl:when test="$name='arrow'">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+     <FONT color="blue" FACE="symbol">
+      <xsl:text>&#x00ae;</xsl:text>
+     </FONT>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
+    <!-- APP -->
+    <xsl:when test="$name='app'">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+     <xsl:for-each select="*[position()>2]">
+      <xsl:text>&#x00A0;</xsl:text>
+      <xsl:apply-templates mode="inline" select="."/>
+     </xsl:for-each>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
+    <!-- CAST -->
+    <xsl:when test="$name='cast'">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+     <xsl:text>:></xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
+    <xsl:when test="$name='Prop'">
+     <FONT color="violet">Prop</FONT>
+    </xsl:when>
+    <xsl:when test="$name='Set'">
+     <FONT color="violet">Set</FONT>
+    </xsl:when>
+    <xsl:when test="$name='Type'">
+     <FONT color="violet">Type</FONT>
+    </xsl:when>
+    <!-- MUTCASE -->
+    <xsl:when test="$name='mutcase'">
+     <xsl:text>&lt;</xsl:text> 
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/> 
+     <xsl:text>&gt; </xsl:text>
+     <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: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="+2" mathcolor="green">&#222;</FONT>
+      <xsl:apply-templates mode="inline"
+           select="following-sibling::*[position()= 1]"/>
+     </xsl:for-each>
+    </xsl:when>
+    <!-- FIX -->
+    <xsl:when test="$name='fix'">
+     <FONT color="red">FIX</FONT>
+     <xsl:value-of select="m:ci"/>
+     <xsl:text>{</xsl:text>
+     <xsl:for-each select="m:bvar"> 
+      <xsl:value-of select="m:ci"/>
+      <xsl:text>:</xsl:text>
+      <xsl:apply-templates mode="inline" select="m:type"/>
+      <xsl:text>:=</xsl:text>
+      <xsl:apply-templates mode="inline" 
+             select="following-sibling::*[position() = 1]"/>
+      <xsl:choose>
+       <xsl:when test="position()=last()">
+        <xsl:text>}</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>;</xsl:text>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:for-each>
+    </xsl:when>
+    <!-- COFIX -->
+    <xsl:when test="$name='cofix'">
+     <xsl:text>COFIX</xsl:text>
+     <xsl:value-of select="m:ci"/>
+     <xsl:text>{</xsl:text>
+     <xsl:for-each select="m:bvar"> 
+      <xsl:value-of select="m:ci"/>
+      <xsl:text>:</xsl:text>
+      <xsl:apply-templates mode="inline" select="m:type"/>
+      <xsl:text>:=</xsl:text>
+      <xsl:apply-templates mode="inline" 
+          select="following-sibling::*[position() = 1]"/>
+      <xsl:choose>
+       <xsl:when test="position()=last()">
+        <xsl:text>}</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>;</xsl:text>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:for-each>
+    </xsl:when>
+    <!-- proof -->
+    <xsl:when test="$name='proof'">
+       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+       <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
+       <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+    </xsl:when>
+    <!-- and_ind -->
+    <xsl:when test="$name='and_ind'">
+     <FONT color="red">From&#x00a0;</FONT>
+     <xsl:apply-templates select="*[2]"/>
+     <FONT color="red">&#x00a0;we get</FONT>
+     (
+     <xsl:apply-templates select="*[3]"/>
+     )&#x00a0;
+     <xsl:apply-templates mode="inline" select="*[4]"/>
+     <FONT color="red">&#x00a0;and&#x00a0;</FONT>
+     (
+     <xsl:apply-templates select="*[5]"/>
+     )&#x00a0;
+     <xsl:apply-templates mode="inline" select="*[6]"/>
+     ;
+     <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
+     <xsl:apply-templates mode="inline" select="*[7]"/>
+    </xsl:when>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template mode="inline" match="m:lambda">
+      <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
+      <xsl:apply-templates select="m:bvar/m:ci"/>
+      <xsl:text>:</xsl:text>
+      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+      <xsl:text>.</xsl:text>
+      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+</xsl:template>
+
+<!--*********************************************************************-->
+<!--                       COUNTING MODE                                 -->
+<!--*********************************************************************-->
+
 <xsl:template match="m:apply[m:csymbol]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/> 
@@ -94,17 +326,43 @@
      <!-- <xsl:value-of select="$current_indent"/> -->
      <!-- <xsl:value-of select="$charlength"/> -->
      <xsl:choose>
-      <xsl:when test="$name='prod'">
+     <!-- FORALL -->
+      <xsl:when test="$name='forall'">
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
          <!-- &#x03a0; -->
-         <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
+         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x22;</FONT>
+         <xsl:apply-templates select="m:bvar/m:ci"/>
+         <xsl:text>:</xsl:text>
+         <xsl:apply-templates select="m:bvar/m:type">
+          <xsl:with-param name="current_indent" 
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
+         </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>.</xsl:text>
+         <xsl:apply-templates select="*[position()=3]">
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+         </xsl:apply-templates>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:apply-templates mode="inline" select="."/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <!-- PROD -->
+      <xsl:when test="$name='prod'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+         <FONT FACE="Symbol" SIZE="+2" color="blue">&#x00d5;</FONT>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
           <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
-         </xsl:apply-templates><BR/> 
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
+         </xsl:apply-templates><br/> 
          <xsl:call-template name="make_indent">
           <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
          </xsl:call-template>
@@ -114,16 +372,11 @@
          </xsl:apply-templates>
        </xsl:when>
        <xsl:otherwise>
-        <!-- &#x03a0; -->
-        <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
-        <xsl:apply-templates select="m:bvar/m:ci"/>
-        <xsl:text>:</xsl:text>
-        <xsl:apply-templates select="m:bvar/m:type"/>
-        <xsl:text>.</xsl:text>
-        <xsl:apply-templates select="*[position()=3]"/>
+        <xsl:apply-templates mode="inline" select="."/>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- ARROW -->
       <xsl:when test="$name='arrow'">
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
@@ -131,27 +384,25 @@
        <xsl:apply-templates select="*[position()=2]">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
        </xsl:apply-templates>
-       <BR/>
+       <br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
        </xsl:call-template>
        <!-- -> -->
-       <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
+       <FONT color="blue" FACE="symbol">
+        <xsl:text>&#x00ae;</xsl:text>
+       </FONT>
        <xsl:apply-templates select="*[position()=3]">
         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
        </xsl:apply-templates>
        <xsl:text>)</xsl:text>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>(</xsl:text>
-        <xsl:apply-templates select="*[position()=2]"/>
-        <!-- -> -->
-        <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
-        <xsl:apply-templates select="*[position()=3]"/>
-        <xsl:text>)</xsl:text>
+        <xsl:apply-templates mode="inline" select="."/>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- APP -->
       <xsl:when test="$name='app'">
        <xsl:choose>
        <xsl:when test="$charlength  > $framewidth">
@@ -160,7 +411,7 @@
          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
         </xsl:apply-templates>
          <xsl:for-each select="*[position()>2]">
-          <BR/>
+          <br/>
            <xsl:call-template name="make_indent">
             <xsl:with-param name="current_indent" select="$current_indent + 2"/>         
            </xsl:call-template>
@@ -171,13 +422,7 @@
          <xsl:text>)</xsl:text>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>(</xsl:text>
-        <xsl:apply-templates select="*[position()=2]"/>
-        <xsl:for-each select="*[position()>2]">
-         <xsl:text>&#x00A0;</xsl:text>
-         <xsl:apply-templates select="."/>
-        </xsl:for-each>
-        <xsl:text>)</xsl:text>
+        <xsl:apply-templates mode="inline" select="."/>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
@@ -189,7 +434,7 @@
            <xsl:text>(</xsl:text>
            <xsl:apply-templates select="*[position()=2]">
             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-           </xsl:apply-templates><BR/>
+           </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>:></xsl:text>
@@ -199,11 +444,7 @@
            <xsl:text>)</xsl:text>
           </xsl:when>
           <xsl:otherwise>
-           <xsl:text>(</xsl:text>
-           <xsl:apply-templates select="*[position()=2]"/>
-           <xsl:text>:></xsl:text>
-           <xsl:apply-templates select="*[position()=3]"/>
-           <xsl:text>)</xsl:text>
+           <xsl:apply-templates mode="inline" select="."/>
           </xsl:otherwise>
          </xsl:choose>
         </xsl:when>
@@ -237,7 +478,7 @@
          </xsl:apply-templates>
          <xsl:text> OF </xsl:text> 
          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
-         <BR/>
+         <br/>
          <xsl:call-template name="make_indent">
             <xsl:with-param name="current_indent" select="$current_indent + 2"/>  
          </xsl:call-template> 
@@ -250,34 +491,18 @@
             </xsl:otherwise>
             </xsl:choose>
             <xsl:apply-templates select="."/>
-            <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
+            <FONT FACE="Symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
             <xsl:apply-templates select="following-sibling::*[position()= 1]">
              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
             </xsl:apply-templates>
          </xsl:for-each>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>&lt;</xsl:text> 
-        <xsl:apply-templates select="*[position()=2]"/> 
-        <xsl:text>&gt; </xsl:text>
-        <xsl:text>CASE </xsl:text>
-        <xsl:apply-templates select="*[position()=3]"/>
-        <xsl:text> OF </xsl:text>
-        <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 select="."/>
-         <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
-         <xsl:apply-templates select="following-sibling::*[position()= 1]">
-          <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
-         </xsl:apply-templates>
-        </xsl:for-each>
+        <xsl:apply-templates mode="inline" select="."/> 
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- FIX -->
       <xsl:when test="$name='fix'">
        <xsl:choose>
        <xsl:when test="$charlength  > $framewidth">
@@ -285,7 +510,7 @@
             <xsl:value-of select="m:ci"/>
             <xsl:text>{</xsl:text> 
             <xsl:for-each select="m:bvar"> 
-              <BR/>
+              <br/>
               <xsl:call-template name="make_indent">
                <xsl:with-param name="current_indent" select="$current_indent + 2"/>  
               </xsl:call-template>
@@ -295,7 +520,7 @@
                <xsl:with-param name="current_indent" 
                     select="$current_indent + 5 + string-length(m:ci)"/>
                </xsl:apply-templates>
-              <BR/>
+              <br/>
               <xsl:call-template name="make_indent">
                <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
               </xsl:call-template>
@@ -304,41 +529,25 @@
                <xsl:with-param name="current_indent" select="$current_indent +2"/>
               </xsl:apply-templates>
             </xsl:for-each>
-             <BR/>
+             <br/>
               <xsl:call-template name="make_indent">
                <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
               </xsl:call-template> 
            <xsl:text>}</xsl:text>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>FIX</xsl:text>
-        <xsl:value-of select="m:ci"/>
-        <xsl:text>{</xsl:text>
-        <xsl:for-each select="m:bvar"> 
-            <xsl:value-of select="m:ci"/>
-            <xsl:text>:</xsl:text>
-            <xsl:apply-templates select="m:type"/>
-            <xsl:text>:=</xsl:text>
-            <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
-            <xsl:choose>
-             <xsl:when test="position()=last()">
-             <xsl:text>}</xsl:text>
-             </xsl:when>
-             <xsl:otherwise>
-             <xsl:text>;</xsl:text>
-             </xsl:otherwise>
-            </xsl:choose>
-         </xsl:for-each>
+        <xsl:apply-templates mode="inline" select="."/>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when> 
+      <!-- COFIX -->
       <xsl:when test="$name='cofix'">
        <xsl:choose>
        <xsl:when test="($charlength + 10) > $framewidth">
             <xsl:text>COFIX</xsl:text>
             <xsl:value-of select="m:ci"/>
             <xsl:text>{</xsl:text>
-            <BR/>
+            <br/>
             <xsl:call-template name="make_indent">
              <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
             </xsl:call-template>
@@ -349,7 +558,7 @@
                  <xsl:with-param name="current_indent" 
                     select="$current_indent + 5 + string-length(m:ci)"/>
                 </xsl:apply-templates>
-                <BR/> 
+                <br/> 
                 <xsl:call-template name="make_indent">
                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
                 </xsl:call-template>
@@ -359,36 +568,234 @@
                 </xsl:apply-templates>
  
             </xsl:for-each>
-            <BR/>
+            <br/>
               <xsl:call-template name="make_indent">
                <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
               </xsl:call-template>
             <xsl:text>}</xsl:text>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>COFIX</xsl:text>
-        <xsl:value-of select="m:ci"/>
-        <xsl:text>{</xsl:text>
-        <xsl:for-each select="m:bvar"> 
-            <xsl:value-of select="m:ci"/>
-            <xsl:text>:</xsl:text>
-            <xsl:apply-templates select="m:type"/>
-            <xsl:text>:=</xsl:text>
-            <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
-            <xsl:choose>
-             <xsl:when test="position()=last()">
-             <xsl:text>}</xsl:text>
-             </xsl:when>
-             <xsl:otherwise>
-             <xsl:text>;</xsl:text>
-             </xsl:otherwise>
-            </xsl:choose>
-         </xsl:for-each>
+        <xsl:apply-templates mode="inline" select="m:type"/>
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
-      </xsl:choose>
-    <!--  </m:mrow> -->
+      <!-- ***************************************** -->
+      <!-- *********** PROOF ELEMENTS ************** -->
+      <!-- ***************************************** -->
+      <!-- PROOF -->
+      <xsl:when test="$name='proof'">
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+       <br/>
+       <!-- <xsl:element name="br"/> -->
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">we proved&#x00a0;</FONT>
+       <xsl:apply-templates select="*[position()=3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 16"/>
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- letin1 -->
+      <xsl:when test="$name='letin1'">
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <xsl:apply-templates select="*[position()=3]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- letin -->
+      <xsl:when test="$name='letin'">
+       <xsl:for-each select="*[position()>1 and last()>position()]">
+        <xsl:apply-templates select=".">
+         <xsl:with-param name="current_indent" select="$current_indent"/>
+        </xsl:apply-templates>
+        <br/>
+        <xsl:call-template name="make_indent">
+         <xsl:with-param name="current_indent" select="$current_indent"/> 
+        </xsl:call-template>
+       </xsl:for-each>
+       <xsl:apply-templates select="*[position()=last()]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- Let -->
+      <xsl:when test="$name='let'">
+       (
+       <xsl:apply-templates select="m:ci"/>
+       )
+       <xsl:apply-templates select="*[3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- rw_step -->
+      <xsl:when test="$name='rw_step'">
+       <xsl:choose>
+        <xsl:when test="name(*[2])='m:apply'">
+         <xsl:apply-templates select="*[2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:apply-templates>
+        </xsl:when>
+        <xsl:otherwise>
+         <FONT color="red">Consider&#x00a0;</FONT>
+         <xsl:apply-templates select="*[2]"/>
+        </xsl:otherwise>
+       </xsl:choose>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">Rewrite&#x00a0;</FONT>
+       <xsl:apply-templates select="*[3]"/>
+       <FONT color="red">&#x00a0;with&#x00a0;</FONT>
+       <xsl:apply-templates select="*[4]"/>
+       <FONT color="red">&#x00a0;by&#x00a0;</FONT>
+       <xsl:apply-templates select="*[5]"/>
+      </xsl:when>
+      <!-- rewrite and apply -->
+      <xsl:when test="$name='rewrite_and_apply'">
+       <xsl:apply-templates select="*[2]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">Then apply it to&#x00a0;</FONT>
+       <xsl:apply-templates select="*[position()>2]"/>
+      </xsl:when>
+      <!-- and_ind -->
+      <xsl:when test="$name='and_ind'">
+       <xsl:choose>
+        <xsl:when test="name(*[2])='m:apply'">
+         <xsl:apply-templates select="*[2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:apply-templates>      
+        </xsl:when>
+        <xsl:otherwise>
+         <FONT color="red">Consider&#x00a0;</FONT>
+         <xsl:apply-templates select="*[2]"/>
+        </xsl:otherwise>
+       </xsl:choose>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">In particular, we have</FONT>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       (
+       <xsl:apply-templates select="*[3]"/>
+       )&#x00a0;
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       (
+       <xsl:apply-templates select="*[5]"/>
+       )&#x00a0;
+       <xsl:apply-templates select="*[6]">
+        <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <xsl:apply-templates select="*[7]">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- or_ind -->
+      <xsl:when test="$name='or_ind'">
+       <xsl:choose>
+        <xsl:when test="name(*[2])='m:apply'">
+         <xsl:apply-templates select="*[2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/> 
+         </xsl:apply-templates>
+        </xsl:when>
+        <xsl:otherwise>
+         <FONT color="red">Consider&#x00a0;</FONT>
+         <xsl:apply-templates select="*[2]"/>
+        </xsl:otherwise>
+       </xsl:choose>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">We prove&#x00a0;</FONT>
+       <xsl:apply-templates select="*[3]"/>
+       <FONT color="red">&#x00a0;by cases:</FONT>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       *
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       *
+       <xsl:apply-templates select="*[5]">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:apply-templates>
+      </xsl:when>
+      <!-- Ex_ind -->
+      <xsl:when test="$name='ex_ind'">
+       <xsl:choose>
+        <xsl:when test="name(*[2])='m:apply'">
+         <xsl:apply-templates select="*[2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:apply-templates>
+        </xsl:when>
+        <xsl:otherwise>
+         <FONT color="red">Consider&#x00a0;</FONT>
+         <xsl:apply-templates select="*[2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:apply-templates>
+        </xsl:otherwise>
+       </xsl:choose>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <FONT color="red">Let&#x00a0;</FONT>
+       <xsl:apply-templates mode="inline" select="*[3]"/>
+       :
+       <xsl:apply-templates mode="inline" select="*[4]"/>
+       <FONT color="red">&#x00a0;such that</FONT>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       (
+       <xsl:apply-templates mode="inline" select="*[5]"/>
+       )
+       <xsl:apply-templates select="*[6]">
+        <xsl:with-param name="current_indent" select="$current_indent +7"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <xsl:apply-templates select="*[7]">
+        <xsl:with-param name="current_indent" select="$current_indent"/>
+       </xsl:apply-templates>
+      </xsl:when>
+     </xsl:choose>
 </xsl:template>
 
 <!-- LAMBDA -->
@@ -400,16 +807,17 @@
      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
     </xsl:variable>
     <!-- <xsl:value-of select="$charlength"/> -->
+    <!-- <xsl:value-of select="$current_indent"/> -->
      <xsl:choose>
      <xsl:when test="$charlength > $framewidth">
        <!-- &#x03bb; -->
-       <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
+       <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
        <xsl:apply-templates select="m:bvar/m:ci"/>
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">
         <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
-       </xsl:apply-templates><BR/> 
+           select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
+       </xsl:apply-templates><br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
        </xsl:call-template>
@@ -419,13 +827,7 @@
        </xsl:apply-templates>
      </xsl:when>
      <xsl:otherwise>
-      <!-- &#x03bb; -->
-      <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
-      <xsl:apply-templates select="m:bvar/m:ci"/>
-      <xsl:text>:</xsl:text>
-      <xsl:apply-templates select="m:bvar/m:type"/>
-      <xsl:text>.</xsl:text>
-      <xsl:apply-templates select="*[position()=2]"/>
+      <xsl:apply-templates mode="inline" select="."/>
      </xsl:otherwise>
      </xsl:choose>
 </xsl:template>
@@ -434,14 +836,11 @@
 <xsl:template match="m:ci">
  <xsl:choose>
   <xsl:when test="boolean(@definitionURL)">
-<!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
-<!--   <xsl:variable name="url">
-    <xsl:value-of select="concat(string($absPath),
-     @definitionURL)"/>
-   </xsl:variable>-->
    <a>
    <xsl:attribute name="href">
-    <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
+    <xsl:call-template name="makeURL">
+     <xsl:with-param name="url" select="@definitionURL"/>
+    </xsl:call-template>
    </xsl:attribute>
    <xsl:apply-templates/>
    </a>
@@ -512,15 +911,15 @@
 <xsl:template match="Definition">
 <xsl:param name="current_indent" select="0"/>
 <p>
-DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
-TYPE =<BR/>
+DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
+TYPE =<br/>
       <xsl:call-template name="make_indent">
        <xsl:with-param name="current_indent" select="$current_indent + 7"/> 
       </xsl:call-template>
        <xsl:apply-templates select="type/*[1]">
         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
-       </xsl:apply-templates><BR/>
-BODY =<BR/>
+       </xsl:apply-templates><br/>
+BODY =<br/>
       <xsl:call-template name="make_indent">
        <xsl:with-param name="current_indent" select="$current_indent + 7"/> 
       </xsl:call-template>
@@ -535,8 +934,12 @@ BODY =<BR/>
 <xsl:template match="Axiom">
 <xsl:param name="current_indent" select="0"/>
 <p>
-AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
-TYPE = <xsl:apply-templates select="type/*[1]">
+AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
+TYPE =<br/>
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 7"/> 
+      </xsl:call-template> 
+<xsl:apply-templates select="type/*[1]">
           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
        </xsl:apply-templates>
 </p>
@@ -547,13 +950,13 @@ TYPE = <xsl:apply-templates select="type/*[1]">
 <xsl:template match="CurrentProof">
 <xsl:param name="current_indent" select="0"/>
 <p>
-UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
+UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
 THESIS:  <xsl:apply-templates select="type/*[1]">
           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
-         </xsl:apply-templates><BR/>
+         </xsl:apply-templates><br/>
 CONJECTURES: 
       <xsl:for-each select="Conjecture">
-      <BR/>
+      <br/>
       <xsl:call-template name="make_indent">
        <xsl:with-param name="current_indent" select="$current_indent + 8"/> 
       </xsl:call-template>
@@ -562,7 +965,7 @@ CONJECTURES:
        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
       </xsl:apply-templates>
       </xsl:for-each> 
-      <BR/>
+      <br/>
 PROOF:
       <xsl:apply-templates select="body/*[1]">
         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
@@ -600,14 +1003,14 @@ PROOF:
             <xsl:apply-templates select="*"/>
            </xsl:for-each>
           </xsl:if>
-         ] <BR/>
+         ] <br/>
          OF ARITY 
          <xsl:apply-templates select="./arity/*[1]">
           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
-         </xsl:apply-templates> <BR/>
+         </xsl:apply-templates> <br/>
          BUILT FROM:
       <xsl:for-each select="./Constructor">
-      <BR/>
+      <br/>
       <xsl:call-template name="make_indent">
        <xsl:with-param name="current_indent" select="$current_indent + 3"/> 
       </xsl:call-template>
@@ -619,10 +1022,10 @@ PROOF:
          <xsl:text>| </xsl:text>
          </xsl:otherwise>
          </xsl:choose>
-         <xsl:value-of select="./@name"/> 
+         <xsl:value-of select="./@name"/>
          <xsl:text>: </xsl:text>
          <xsl:apply-templates select="./*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+          <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
          </xsl:apply-templates>
       </xsl:for-each>
      </xsl:for-each>
@@ -634,7 +1037,7 @@ PROOF:
 <xsl:template match="Variable">
 <xsl:param name="current_indent" select="0"/>
 <p>
-VARIABLE <xsl:value-of select="@name"/><BR/>
+VARIABLE <xsl:value-of select="@name"/><br/>
 TYPE = <xsl:apply-templates select="type/*[1]">
           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
        </xsl:apply-templates>