]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 10c1185)
New stylesheets from content to html.
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 20 Feb 2001 10:30:36 +0000 (10:30 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 20 Feb 2001 10:30:36 +0000 (10:30 +0000)
-- andrea

helm/style/content_to_html.xsl patch | blob | history
helm/style/html_init.xsl patch | blob | history
helm/style/html_reals.xsl patch | blob | history
helm/style/html_set.xsl patch | blob | history
helm/style/mmlextension.xsl patch | blob | history

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 5b57eb0ff19859363a9c0d74bf25ee064bed9877..62a4936f0c071e83f6b74fa5da0061a2769a39c3 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -32,6 +32,12 @@
 <!-- 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:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
+
+<xsl:variable name="header"><xsl:value-of select="$processorURL"/>/apply?key=C1&#x26;key=HC2&#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"/>
@@ -44,15 +50,20 @@
 <!-- HTML Head and Body                                                    -->
 <!--***********************************************************************-->
 
-<xsl:output method="html"/>
+<!-- <xsl:output method="html"/> -->
+<xsl:output method="html" encoding="iso-8859-1"/>
 
 <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>
@@ -67,7 +78,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>
@@ -75,7 +86,6 @@
 </xsl:template>
 
 <!-- Syntactic Sugar -->
-
 <xsl:template match="m:type">
 <xsl:param name="current_indent" select="0"/> 
 <xsl:apply-templates>
@@ -100,8 +110,173 @@
 </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:value-of select="concat(string($header),string(@definitionURL))"/>
+   </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>
+    <xsl:when test="$name='proof'">
+       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+       <FONT color="red">we proved</FONT>
+       <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+    </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"/> 
@@ -114,17 +289,19 @@
      <!-- <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" mathcolor="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 + 2 + string-length(m:bvar/m:ci)"/>
-         </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>
@@ -134,16 +311,35 @@
          </xsl:apply-templates>
        </xsl:when>
        <xsl:otherwise>
-        <!-- &#x03a0; -->
-        <FONT FACE="symbol" SIZE="+2" mathcolor="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>
+      <!-- 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/> 
+         <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>
+      <!-- ARROW -->
       <xsl:when test="$name='arrow'">
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
@@ -151,27 +347,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" mathcolor="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" mathcolor="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">
@@ -180,7 +374,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>
@@ -191,13 +385,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>
@@ -209,7 +397,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>
@@ -219,11 +407,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>
@@ -257,7 +441,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> 
@@ -270,34 +454,18 @@
             </xsl:otherwise>
             </xsl:choose>
             <xsl:apply-templates select="."/>
-            <FONT FACE="symbol" SIZE="+2" mathcolor="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" mathcolor="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">
@@ -305,7 +473,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>
@@ -315,7 +483,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>
@@ -324,41 +492,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>
@@ -369,7 +521,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>
@@ -379,36 +531,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'">
+       <m:mtext>(</m:mtext>
+       <xsl:apply-templates select="m:ci"/>
+       <m:mtext>) </m:mtext>
+       <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>
+       <m:mtext>(</m:mtext>
+       <xsl:apply-templates select="*[3]"/>
+       <m:mtext>)&#x00a0;</m:mtext>
+       <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>
+       <m:mtext>(</m:mtext>
+       <xsl:apply-templates select="*[5]"/>
+       <m:mtext>)&#x00a0;</m:mtext>
+       <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>
+       <m:mtext>*</m:mtext>
+       <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>
+       <m:mtext>*</m:mtext>
+       <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]"/>
+       <m:mtext>:</m:mtext>
+       <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>
+       <m:mtext>(</m:mtext>
+       <xsl:apply-templates mode="inline" select="*[5]"/>
+       <m:mtext>)</m:mtext>
+       <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 -->
@@ -420,16 +770,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" mathcolor="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/> 
+       </xsl:apply-templates><br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
        </xsl:call-template>
@@ -439,13 +790,7 @@
        </xsl:apply-templates>
      </xsl:when>
      <xsl:otherwise>
-      <!-- &#x03bb; -->
-      <FONT FACE="symbol" SIZE="+2" mathcolor="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>
@@ -454,11 +799,6 @@
 <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))"/>
@@ -532,15 +872,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>
@@ -555,8 +895,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>
@@ -567,13 +911,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>
@@ -582,7 +926,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"/>
@@ -620,14 +964,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>
@@ -654,7 +998,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>
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index bb6bea3ba064347478c777b5c9c2f91d6c1b65fa..f52525ebf3eb80f20a52e190a542c97ecd35dcff 100644 (file)
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -32,6 +32,128 @@
 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
 <!--***********************************************************************--> 
 
+<!-- INLINE MODE : BASIC OPERATORS -->
+
+ <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
+       |m:geq|m:gt|m:plus|m:times]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
+  </xsl:variable>
+  <xsl:variable name="symbol">
+   <xsl:choose>
+    <xsl:when test="m:and">
+     <xsl:value-of select="'&#217;'"/>
+    </xsl:when>
+    <xsl:when test="m:or">
+     <xsl:value-of select="'&#218;'"/>
+    </xsl:when>
+    <xsl:when test="m:eq">
+     <xsl:value-of select="'&#61;'"/>
+    </xsl:when>
+    <xsl:when test="m:neq">
+     <xsl:value-of select="'&#185;'"/>
+    </xsl:when>
+    <xsl:when test="m:leq">
+     <xsl:value-of select="'&#163;'"/>
+    </xsl:when>
+    <xsl:when test="m:lt">
+     <xsl:value-of select="'&#60;'"/>
+    </xsl:when>
+    <xsl:when test="m:geq">
+     <xsl:value-of select="'&#179;'"/>
+    </xsl:when>
+    <xsl:when test="m:gt">
+     <xsl:value-of select="'&#62;'"/>
+    </xsl:when>
+    <xsl:when test="m:plus">
+     <xsl:value-of select="'&#43;'"/>
+    </xsl:when>
+    <xsl:when test="m:times">
+     <xsl:value-of select="'&#42;'"/>
+    </xsl:when>
+   </xsl:choose>
+  </xsl:variable>
+  <xsl:text>(</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <a>
+   <xsl:attribute name="href">
+    <xsl:value-of select="concat(string($header),string($uri))"/>
+   </xsl:attribute>
+   <FONT FACE="symbol" mathcolor="blue">
+    <xsl:value-of select="$symbol"/>
+   </FONT>
+  </a>
+  <xsl:apply-templates mode="inline" select="*[3]"/>
+  <xsl:text>)</xsl:text>
+ </xsl:template>
+
+<!-- INLINE MODE - MINUS (can be unary!) -->
+
+<xsl:template mode="inline" match="m:apply[m:minus]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="count(child::*)=2">
+    <a>
+    <xsl:attribute name="href">
+     <xsl:value-of select="concat(string($header),string($uri))"/>
+    </xsl:attribute>
+    <xsl:text>-</xsl:text>
+    </a>
+    <xsl:apply-templates mode="inline" select="*[2]"/>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:text>(</xsl:text>
+    <xsl:apply-templates mode="inline" select="*[2]"/>
+    <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <xsl:text>-</xsl:text>
+    </a>
+    <xsl:apply-templates mode="inline" select="*[3]"/>
+    <xsl:text>)</xsl:text>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:template>
+
+<!-- INLINE MODE NOT -->
+
+ <xsl:template mode="inline" match="m:apply[m:not]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:not/@definitionURL"/>
+  </xsl:variable>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
+     </a>
+     <xsl:apply-templates mode="inline" select="*[2]"/>
+ </xsl:template>
+
+<!-- INLINE MODE EXISTS -->
+
+ <xsl:template mode="inline" match="m:apply[m:exists]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:exists/@definitionURL"/>
+  </xsl:variable>
+  <a>
+   <xsl:attribute name="href">
+    <xsl:value-of select="concat(string($header),string($uri))"/>
+   </xsl:attribute>
+   <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
+  </a>
+  <xsl:apply-templates select="m:bvar/m:ci"/>
+  <xsl:text>:</xsl:text>
+  <xsl:apply-templates mode="inline" select="m:condition"/>
+  <xsl:text>.</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[last()]"/>
+ </xsl:template>
+
+<!-- COUNTING MODE -->
+
 <!-- BASIC OPERATORS -->
 
  <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
@@ -102,18 +224,7 @@
      <xsl:text>)</xsl:text>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" mathcolor="blue">
-     <xsl:value-of select="$symbol"/>
-     </FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
+     <xsl:apply-templates mode="inline" select="."/>
     </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
@@ -164,16 +275,7 @@
       <xsl:text>)</xsl:text>
      </xsl:when>
      <xsl:otherwise>
-      <xsl:text>(</xsl:text>
-      <xsl:apply-templates select="*[2]"/>
-      <a>
-      <xsl:attribute name="href">
-       <xsl:value-of select="concat(string($header),string($uri))"/>
-      </xsl:attribute>
-      <xsl:text>-</xsl:text>
-      </a>
-      <xsl:apply-templates select="*[3]"/>
-      <xsl:text>)</xsl:text>
+      <xsl:apply-templates mode="inline" select="."/>
      </xsl:otherwise>
     </xsl:choose>
    </xsl:otherwise>
@@ -232,19 +334,7 @@
       </xsl:apply-templates>
     </xsl:when>
     <xsl:otherwise>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
-     </a>
-     <xsl:apply-templates select="m:bvar/m:ci"/>
-     <xsl:text>:</xsl:text>
-     <xsl:apply-templates select="m:condition"/>
-     <xsl:text>.</xsl:text>
-     <xsl:apply-templates select="*[last()]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
+     <xsl:apply-templates mode="inline" select="."/>
     </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl
index de3196b128118af37f2538009623f992a92449a5..2b4ca35e5a742f1209f2f58ef128d7e8e99046ab 100644 (file)
--- a/helm/style/html_reals.xsl
+++ b/helm/style/html_reals.xsl
@@ -32,8 +32,128 @@
 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
 <!--***********************************************************************--> 
 
+<!-- **************************************************************** -->
+<!--                   INLINE MODE                                    -->
+<!-- **************************************************************** -->
+
 <!-- LIMIT -->
 
+
+<xsl:template mode="inline" match="m:apply[m:limit]">
+     <xsl:variable name="uri">
+      <xsl:value-of select="m:limit/@definitionURL"/>
+     </xsl:variable>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <xsl:text>lim</xsl:text>
+     </a>
+     <SUB>
+      <xsl:apply-templates select="m:bvar/m:ci"/>
+      <FONT FACE="symbol" mathcolor="blue">&#174;</FONT>
+      <xsl:apply-templates mode="inline" select="m:lowlimit"/>
+     </SUB>
+     <xsl:apply-templates mode="inline" select="*[4]"/>
+ </xsl:template>
+
+<!-- DIFFERENTIATION -->
+
+<xsl:template mode="inline" match="m:apply[m:diff]">
+     <xsl:variable name="uri">
+      <xsl:value-of select="m:diff/@definitionURL"/>
+     </xsl:variable>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <SUP>d</SUP>
+      <xsl:text>/</xsl:text>
+     <SUB>
+      <xsl:text>d</xsl:text>
+      <xsl:value-of select="m:bvar/m:ci"/>
+     </SUB>
+     </a>
+     <xsl:apply-templates mode="inline" select="*[3]"/>
+ </xsl:template>
+
+<!-- ABSOLUTE VALUE -->
+<xsl:template mode="inline" match="m:apply[m:abs]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:abs/@definitionURL"/>
+  </xsl:variable>
+  <xsl:text>|</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <xsl:text>|</xsl:text>
+</xsl:template>
+
+<!-- FACTORIAL -->
+
+<xsl:template mode="inline" match="m:apply[m:fact]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:abs/@definitionURL"/>
+  </xsl:variable>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <xsl:text>!</xsl:text>
+</xsl:template>
+
+<!-- SQUARE ROOT -->
+
+<xsl:template match="m:apply[m:root]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:abs/@definitionURL"/>
+  </xsl:variable>
+  <xsl:text>(sqr</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <xsl:text>)</xsl:text>
+</xsl:template>
+
+<!-- POWER -->
+
+<xsl:template mode="inline" match="m:apply[m:power]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:power/@definitionURL"/>
+  </xsl:variable>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <SUP>
+  <xsl:apply-templates mode="inline" select="*[3]"/>
+  </SUP>
+</xsl:template>
+
+<!-- MIN and MAX (binari: estendere) -->
+
+ <xsl:template mode="inline" match="m:apply[m:min|m:max]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
+  </xsl:variable>
+  <xsl:variable name="symbol">
+   <xsl:choose>
+    <xsl:when test="m:min">
+     <xsl:value-of select="'min'"/>
+    </xsl:when>
+    <xsl:when test="m:max">
+     <xsl:value-of select="'max'"/>
+    </xsl:when>
+   </xsl:choose>
+  </xsl:variable>
+  <a>
+   <xsl:attribute name="href">
+    <xsl:value-of select="concat(string($header),string($uri))"/>
+   </xsl:attribute>
+   <xsl:value-of select="$symbol"/>
+  </a>
+  <xsl:text>{</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <xsl:text>, </xsl:text>
+  <xsl:apply-templates mode="inline" select="*[3]"/>
+  <xsl:text>}</xsl:text>
+</xsl:template>
+
+<!-- **************************************************************** -->
+<!--                   COUNTING MODE                                    -->
+<!-- **************************************************************** -->
+
+
 <xsl:template match="m:apply[m:limit]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
@@ -65,26 +185,12 @@
      </xsl:apply-templates>
     </xsl:when>
     <xsl:otherwise>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <xsl:text>lim</xsl:text>
-     </a>
-     <SUB>
-      <xsl:apply-templates select="m:bvar/m:ci"/>
-      <FONT FACE="symbol" mathcolor="blue">&#174;</FONT>
-      <xsl:apply-templates select="m:lowlimit"/>
-     </SUB>
-     <xsl:apply-templates select="*[4]">
-      <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-     </xsl:apply-templates>
+     <xsl:apply-templates mode="inline" select="."/>
     </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
 
 <!-- DIFFERENTIATION -->
-
 <xsl:template match="m:apply[m:diff]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
@@ -107,6 +213,7 @@
      </xsl:apply-templates>
  </xsl:template>
 
+
 <!-- ABSOLUTE VALUE -->
 <xsl:template match="m:apply[m:abs]">
   <xsl:param name="current_indent" select="0"/> 
@@ -208,17 +315,7 @@
      <xsl:text>}</xsl:text>
     </xsl:when>
     <xsl:otherwise>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <xsl:value-of select="$symbol"/>
-     </a>
-     <xsl:text>{</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <xsl:text>, </xsl:text>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>}</xsl:text>
+     <xsl:apply-templates mode="inline" select="."/>
     </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 78f4a5b9ea98e0c01ed0b1c9d7bd8c40b3fc2dbb..97e3b1e074c89197115aefec36bbd6edad638203 100644 (file)
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -32,63 +32,143 @@
 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
 <!--***********************************************************************--> 
 
-<!-- IN -->
+<!-- **************************************************************** -->
+<!--                   INLINE MODE                                    -->
+<!-- **************************************************************** -->
 
- <xsl:template match="m:apply[m:in]">
+<!-- SET -->
+
+ <xsl:template mode="inline" match="m:set">
+  <xsl:variable name="uri">
+   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="count(child::*) = 0">
+    <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:choose>
+     <xsl:when test="name(*[1]) = 'm:bvar'">
+      <xsl:text>{</xsl:text>
+      <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()=2]"/>
+      <xsl:text>}</xsl:text>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:text>{</xsl:text>
+      <xsl:for-each select="*">
+       <xsl:apply-templates mode="inline" select="."/>
+       <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:otherwise>
+    </xsl:choose>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:template>
+
+
+<!-- CARD -->
+<xsl:template mode="inline" match="m:apply[m:card]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
   <xsl:variable name="uri">
-   <xsl:value-of select="m:in/@definitionURL"/>
+   <xsl:value-of select="m:card/@definitionURL"/>
   </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:in" mode="charcount"/>
+  <xsl:text>|</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <xsl:text>|</xsl:text>
+ </xsl:template>
+
+<xsl:template mode="inline" match="m:apply[m:in|m:notin|m:intersect|m:union
+  |m:subset|m:prsubset|m:setdiff]">
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
   </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
+  <xsl:variable name="symbol">
+   <xsl:choose>
+    <xsl:when test="m:in">
+     <xsl:value-of select="'&#206;'"/>
+    </xsl:when>
+    <xsl:when test="m:notin">
+     <xsl:value-of select="'&#207;'"/>
+    </xsl:when>
+    <xsl:when test="m:intersect">
+     <xsl:value-of select="'&#199;'"/>
+    </xsl:when>
+    <xsl:when test="m:union">
+     <xsl:value-of select="'&#200;'"/>
+    </xsl:when>
+    <xsl:when test="m:subset">
+     <xsl:value-of select="'&#205;'"/>
+    </xsl:when>
+    <xsl:when test="m:prsubset">
+     <xsl:value-of select="'&#204;'"/>
+    </xsl:when>
+    <xsl:when test="m:setdiff">
+     <xsl:value-of select="'/'"/>
     </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
    </xsl:choose>
+  </xsl:variable>
+  <xsl:text>(</xsl:text>
+  <xsl:apply-templates mode="inline" select="*[2]"/>
+  <a>
+   <xsl:attribute name="href">
+    <xsl:value-of select="concat(string($header),string($uri))"/>
+   </xsl:attribute>
+   <FONT FACE="symbol" mathcolor="blue">
+    <xsl:value-of select="$symbol"/>
+   </FONT>
+  </a>
+  <xsl:apply-templates mode="inline" select="*[3]"/>
+  <xsl:text>)</xsl:text>
  </xsl:template>
 
-<!-- NOTIN -->
+<!-- *************************************************************** -->
 
- <xsl:template match="m:apply[m:notin]">
+<xsl:template match="m:apply[m:in|m:notin|m:intersect|m:union
+  |m:subset|m:prsubset|m:setdiff]">
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
   <xsl:variable name="uri">
-   <xsl:value-of select="m:notin/@definitionURL"/>
+   <xsl:value-of select="*[1]/@definitionURL"/>
   </xsl:variable>
   <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:notin" mode="charcount"/>
+   <xsl:apply-templates select="*[1]" mode="charcount"/>
+  </xsl:variable>
+  <xsl:variable name="symbol">
+   <xsl:choose>
+    <xsl:when test="m:in">
+     <xsl:value-of select="'&#206;'"/>
+    </xsl:when>
+    <xsl:when test="m:notin">
+     <xsl:value-of select="'&#207;'"/>
+    </xsl:when>
+    <xsl:when test="m:intersect">
+     <xsl:value-of select="'&#199;'"/>
+    </xsl:when>
+    <xsl:when test="m:union">
+     <xsl:value-of select="'&#200;'"/>
+    </xsl:when>
+    <xsl:when test="m:subset">
+     <xsl:value-of select="'&#205;'"/>
+    </xsl:when>
+    <xsl:when test="m:prsubset">
+     <xsl:value-of select="'&#204;'"/>
+    </xsl:when>
+    <xsl:when test="m:setdiff">
+     <xsl:value-of select="'/'"/>
+    </xsl:when>
+   </xsl:choose>
   </xsl:variable>
   <xsl:choose>
     <xsl:when test="$charlength > $framewidth">
@@ -100,22 +180,26 @@
      <xsl:call-template name="make_indent">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" mathcolor="blue">
+      <xsl:value-of select="$symbol"/>
+     </FONT>
+     </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
      </xsl:apply-templates>
      <xsl:text>)</xsl:text>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
+     <xsl:apply-templates mode="inline" select="."/>
     </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
 
+
 <!-- SET -->
 
  <xsl:template match="m:set">
@@ -133,9 +217,9 @@
      <xsl:apply-templates select="." mode="charcount"/>
     </xsl:variable>
     <xsl:choose>
-     <xsl:when test="name(*[1]) = 'm:bvar'">
+     <xsl:when test="$charlength > $framewidth">
       <xsl:choose>
-       <xsl:when test="$charlength > $framewidth">
+       <xsl:when test="name(*[1]) = 'm:bvar'">
         <xsl:text>{</xsl:text>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <xsl:text>:</xsl:text>
@@ -153,19 +237,6 @@
         <xsl:text>}</xsl:text>
        </xsl:when>
        <xsl:otherwise>
-        <xsl:text>{</xsl:text>
-        <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:text>}</xsl:text>
-       </xsl:otherwise>
-      </xsl:choose>
-     </xsl:when>
-     <xsl:otherwise>
-      <xsl:choose>
-       <xsl:when test="$charlength > $framewidth">
         <xsl:text>{</xsl:text>
          <xsl:apply-templates select="*[position()=1]">
           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -180,263 +251,17 @@
            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
           </xsl:apply-templates>
          </xsl:for-each>
-         <xsl:text>}</xsl:text>
-        </xsl:when>
-        <xsl:otherwise>
-        <xsl:text>{</xsl:text>
-         <xsl:for-each select="*">
-          <xsl:apply-templates select="."/>
-          <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:otherwise>
-       </xsl:choose>
-      </xsl:otherwise>
-     </xsl:choose>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
-
-
-<!-- INTERSECTION -->
-
-<xsl:template match="m:apply[m:intersect]">
-  <xsl:param name="current_indent" select="0"/> 
-  <xsl:param name="width" select="$framewidth"/>
-  <xsl:variable name="uri">
-   <xsl:value-of select="m:intersect/@definitionURL"/>
-  </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:intersect" mode="charcount"/>
-  </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
-
-<!-- UNION -->
-
-<xsl:template match="m:apply[m:union]">
-  <xsl:param name="current_indent" select="0"/> 
-  <xsl:param name="width" select="$framewidth"/>
-  <xsl:variable name="uri">
-   <xsl:value-of select="m:union/@definitionURL"/>
-  </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:union" mode="charcount"/>
-  </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
-
-<!-- SUBSET -->
-<xsl:template match="m:apply[m:subset]">
-  <xsl:param name="current_indent" select="0"/> 
-  <xsl:param name="width" select="$framewidth"/>
-  <xsl:variable name="uri">
-   <xsl:value-of select="m:subset/@definitionURL"/>
-  </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:subset" mode="charcount"/>
-  </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
-
-<!-- PRSUBSET -->
-<xsl:template match="m:apply[m:prsubset]">
-  <xsl:param name="current_indent" select="0"/> 
-  <xsl:param name="width" select="$framewidth"/>
-  <xsl:variable name="uri">
-   <xsl:value-of select="m:prsubset/@definitionURL"/>
-  </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:prsubset" mode="charcount"/>
-  </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
-
-
-<!-- SETDIFF -->
-
-<xsl:template match="m:apply[m:setdiff]">
-  <xsl:param name="current_indent" select="0"/> 
-  <xsl:param name="width" select="$framewidth"/>
-  <xsl:variable name="uri">
-   <xsl:value-of select="m:setdiff/@definitionURL"/>
-  </xsl:variable>
-  <xsl:variable name="charlength">
-   <xsl:apply-templates select="m:setdiff" mode="charcount"/>
-  </xsl:variable>
-  <xsl:choose>
-    <xsl:when test="$charlength > $framewidth">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <BR/> 
-     <xsl:call-template name="make_indent">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-     </xsl:call-template>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <xsl:text>/</xsl:text>
-     </a>
-     <xsl:apply-templates select="*[3]">
-      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-     </xsl:apply-templates>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates select="*[2]"/>
-     <a>
-     <xsl:attribute name="href">
-      <xsl:value-of select="concat(string($header),string($uri))"/>
-     </xsl:attribute>
-     <xsl:text>/</xsl:text>
-     </a>
-     <xsl:apply-templates select="*[3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:otherwise>
-   </xsl:choose>
- </xsl:template>
+        <xsl:text>}</xsl:text>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-templates mode="inline" select="."/>
+     </xsl:otherwise>
+    </xsl:choose>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:template> 
 
 <!-- CARD -->
 <xsl:template match="m:apply[m:card]">
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 86675e553e48abf02c18c78ecf1043341445b65f..900dd4bf62fda76d26f9750cb2c91bb9106690e1 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1045,6 +1045,7 @@
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- not existing any more
       <xsl:when test="$name='thread'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1065,7 +1066,8 @@
          </m:mtr>
         <xsl:apply-templates mode="thread" select="*[(last()-2)]"/> 
         </m:mtable>
-      </xsl:when> 
+      </xsl:when>
+      --> 
       <xsl:when test="$name='rewrite_and_apply'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
Unnamed repository; edit this file 'description' to name the repository.