X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fxslt%2Flddl_library.xsl;h=a126c9ba4e1ad38ff935cf639686e7444fa72490;hb=2c4b4aaa6f1490346823a26cba5dd965cab0cd02;hp=ccd977990196e7f79a77f9ecabe6695a094939ed;hpb=edf9e34100f49d4aa5ba8f3ce53e34af7718d88e;p=helm.git

diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl
index ccd977990..a126c9ba4 100644
--- a/helm/www/lambdadelta/xslt/lddl_library.xsl
+++ b/helm/www/lambdadelta/xslt/lddl_library.xsl
@@ -12,26 +12,18 @@
       V_______________________________________________________________ -->
 
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
-                              xmlns:ld="http://lambdadelta.info/"
-                              xmlns="http://www.w3.org/1999/xhtml"
+                              xmlns="http://lambdadelta.info/"
+                              xmlns:xhtml="http://www.w3.org/1999/xhtml"
 >
 
 <xsl:template name="sp">
    <xsl:text> </xsl:text>
 </xsl:template>
 
-<xsl:template name="cm">
-   <xsl:text>, </xsl:text>
-</xsl:template>
-
 <xsl:template name="sl">
    <xsl:text>/</xsl:text>
 </xsl:template>
 
-<xsl:template name="plus">
-   <xsl:text>+</xsl:text>
-</xsl:template>
-
 <xsl:template name="fs">
    <xsl:text>.&#x200B;</xsl:text>
 </xsl:template>
@@ -52,6 +44,14 @@
    <xsl:text>]</xsl:text>
 </xsl:template>
 
+<xsl:template name="oc">
+   <xsl:text>{</xsl:text>
+</xsl:template>
+
+<xsl:template name="cc">
+   <xsl:text>}</xsl:text>
+</xsl:template>
+
 <xsl:template name="oa">
    <xsl:text>&lt;</xsl:text>
 </xsl:template>
@@ -60,6 +60,10 @@
    <xsl:text>&gt;</xsl:text>
 </xsl:template>
 
+<xsl:template name="us">
+   <xsl:text>_</xsl:text>
+</xsl:template>
+
 <xsl:template name="cn">
    <xsl:text>:</xsl:text>
 </xsl:template>
@@ -68,196 +72,72 @@
    <xsl:text>=</xsl:text>
 </xsl:template>
 
-<xsl:template name="qt">
-   <xsl:text>"</xsl:text>
+<xsl:template name="infinity">
+   <xsl:text>∞</xsl:text>
 </xsl:template>
 
-<xsl:template name="idescr">
-   <xsl:text>Informal description: </xsl:text>
+<xsl:template name="lambda">
+   <xsl:text>λ</xsl:text>
 </xsl:template>
 
-<xsl:template name="vpars">
-   <xsl:text>Validation parameters: </xsl:text>
+<xsl:template name="Pi">
+   <xsl:text>Π</xsl:text>
 </xsl:template>
 
-<xsl:template name="shier">
-   <xsl:text>sort hierarchy = </xsl:text>
+<xsl:template name="forall">
+   <xsl:text>∀</xsl:text>
 </xsl:template>
 
-<xsl:template name="kopts">
-   <xsl:text>kernel options = </xsl:text>
+<xsl:template name="delta">
+   <xsl:text>δ</xsl:text>
 </xsl:template>
 
-<xsl:template name="multiple">
-   <span class="separator">
-      <xsl:call-template name="cm"/>
-   </span>
+<xsl:template name="chi">
+   <xsl:text>χ</xsl:text>
 </xsl:template>
 
-<xsl:template name="lambda">
-   <a title="{@mark}">
-      <xsl:choose>
-	 <xsl:when test="@level=0">
-	    <xsl:text disable-output-escaping="yes">&amp;Pi;</xsl:text>
-            <sup><xsl:value-of select="@level"/></sup>
-	 </xsl:when>
-	 <xsl:when test="@level=1">
-	    <xsl:text disable-output-escaping="yes">&amp;Pi;</xsl:text>
-	 </xsl:when>
-	 <xsl:when test="@level=2">
-	    <xsl:text disable-output-escaping="yes">&amp;lambda;</xsl:text>
-	 </xsl:when>
-	 <xsl:when test="not(@level)">
-	    <xsl:text disable-output-escaping="yes">&amp;lambda;</xsl:text>
-	    <sup><xsl:text disable-output-escaping="yes">&amp;infin;</xsl:text></sup>
-	 </xsl:when>
-	 <xsl:otherwise>
-	    <xsl:text disable-output-escaping="yes">&amp;lambda;</xsl:text>
-            <sup><xsl:value-of select="@level"/></sup>
-	 </xsl:otherwise>
-      </xsl:choose>
-   </a>
+<xsl:template name="cm">
+   <xsl:text>, </xsl:text>
 </xsl:template>
 
-<xsl:template name="delta">
-   <a title="{@mark}">
-      <xsl:text disable-output-escaping="yes">&amp;delta;</xsl:text>
-   </a>
+<xsl:template name="qt">
+   <xsl:text>"</xsl:text>
 </xsl:template>
 
-<xsl:template name="chi">
-   <a title="{@mark}">
-      <xsl:text disable-output-escaping="yes">&amp;chi;</xsl:text>
-   </a>
+<xsl:template name="idescr">
+   <xsl:text>Informal description: </xsl:text>
 </xsl:template>
 
-<xsl:template name="position">
-   <xsl:variable name="index">
-      <xsl:value-of select="@position"/>
-      <xsl:if test="@offset != 0">
-         <xsl:call-template name="plus"/>
-	 <xsl:value-of select="@offset"/>
-      </xsl:if>
-   </xsl:variable>
-   <a title="{$index}">
-      <xsl:value-of select="@name"/>
-   </a>
+<xsl:template name="vpars">
+   <xsl:text>Validation parameters: </xsl:text>
 </xsl:template>
 
-<xsl:template name="lddlbaseurl">
-   <xsl:value-of select="$baseurl"/>
-   <xsl:value-of select="'static/lddl'"/>
+<xsl:template name="shier">
+   <xsl:text>sort hierarchy = </xsl:text>
 </xsl:template>
 
-<xsl:template name="uri">
-   <xsl:variable name="url">
-      <xsl:call-template name="lddlbaseurl">
-      <xsl:value-of select="substring-after(@uri,'ld:')"/>
-      <xsl:text>.html</xsl:text>
-   </xsl:variable>
-   <a href="{$url}" title="{@uri}"><xsl:value-of select="@name"/></a>
+<xsl:template name="kopts">
+   <xsl:text>kernel options = </xsl:text>
 </xsl:template>
 
 <xsl:template name="global">
-   <a title="{@mark}">
+   <xhtml:span class="global" title="{@position}">
       <xsl:value-of select="@name"/>
-   </a>
-</xsl:template>
-
-<xsl:template name="mk_names">
-   <xsl:param name="names">
-      <xsl:value-of select="normalize-space(@name)"/>
-      <xsl:call-template name="sp"/>
-   </xsl:param>
-   <xsl:param name="sep" select="false()"/>
-   <xsl:if test="$names and $sep">
-      <xsl:call-template name="multiple"/>
-   </xsl:if>
-   <xsl:if test="$names">
-      <span class="lref">
-         <xsl:value-of select="substring-before($names, ' ')"/>
-      </span>
-      <xsl:call-template name="mk_names">
-         <xsl:with-param name="names" select="substring-after($names, ' ')"/>
-         <xsl:with-param name="sep" select="true()"/>
-      </xsl:call-template>
-   </xsl:if>
-</xsl:template>
-
-<xsl:template name="mk_terms">
-   <xsl:for-each select="*">
-      <xsl:apply-templates select="."/>
-      <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
-         <xsl:call-template name="multiple"/>
-      </xsl:if>
-   </xsl:for-each>
+   </xhtml:span>
 </xsl:template>
 
-<xsl:template name="mk_binder">
-   <xsl:param name="sep-seq"/>
-   <xsl:call-template name="ob"/>
-   <xsl:call-template name="mk_binder_rec1">
-      <xsl:with-param name="sep-seq" select="$sep-seq"/>
-   </xsl:call-template>
-   <xsl:call-template name="cb"/>
-</xsl:template>
-
-<xsl:template name="mk_binder_rec1">
-   <xsl:param name="sep-seq"/>
-   <xsl:param name="names">
-      <xsl:value-of select="normalize-space(@name)"/>
-      <xsl:call-template name="sp"/>
-   </xsl:param>
-   <xsl:param name="sep" select="false()"/>
-   <xsl:param name="start" select="true()"/>
-   <xsl:param name="pos" select="1"/>
-   <xsl:choose>
-      <xsl:when test="$start and $pos &lt;= count(*)">
-         <xsl:if test="$names and $sep">
-            <xsl:call-template name="multiple"/>
-         </xsl:if>
-         <span class="lref">
-	    <xsl:value-of select="substring-before($names, ' ')"/>
-	 </span>
-         <xsl:copy-of select="$sep-seq"/>
-	 <xsl:call-template name="mk_binder_rec2">
-            <xsl:with-param name="names" select="substring-after($names, ' ')"/>
-            <xsl:with-param name="pos" select="$pos"/>
-            <xsl:with-param name="sep-seq" select="$sep-seq"/>
-         </xsl:call-template>
-      </xsl:when>
-      <xsl:when test="not($start) and $pos &lt;= count(*)">
-         <xsl:call-template name="mk_binder_rec2">
-            <xsl:with-param name="names" select="$names"/>
-            <xsl:with-param name="pos" select="$pos"/>
-            <xsl:with-param name="sep-seq" select="$sep-seq"/>
-         </xsl:call-template>
-      </xsl:when>
-   </xsl:choose>
-</xsl:template>
-
-<xsl:template name="mk_binder_rec2">
-   <xsl:param name="sep-seq"/>
-   <xsl:param name="names"/>
-   <xsl:param name="pos"/>
-   <xsl:apply-templates select="*[$pos]"/>
-   <xsl:call-template name="mk_binder_rec1">
-      <xsl:with-param name="sep-seq" select="$sep-seq"/>
-      <xsl:with-param name="names" select="$names"/>
-      <xsl:with-param name="sep" select="true()"/>
-      <xsl:with-param name="start" select="name(*[$pos])='Sort' or name(*[$pos])='LRef' or name(*[$pos])='GRef'"/>
-      <xsl:with-param name="pos" select="$pos+1"/>
-   </xsl:call-template>
+<xsl:template name="lddlurl">
+   <xsl:value-of select="'static/lddl'"/>
 </xsl:template>
 
 <xsl:template name="mk_segment">
    <xsl:param name="path"/>
    <xsl:param name="name"/>
    <xsl:variable name="url">
-      <xsl:call-template name="lddlbaseurl">
+      <xsl:call-template name="lddlurl"/>
       <xsl:value-of select="substring-after($path,'ld:')"/>
    </xsl:variable>
-   <a href="{$url}"><xsl:value-of select="$name"/></a>
+   <rlink to="{$url}"><xsl:value-of select="$name"/></rlink>
    <xsl:call-template name="sl"/>
 </xsl:template>
 
@@ -277,13 +157,119 @@
       </xsl:when>
       <xsl:otherwise>
          <xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
-	 <xsl:value-of select="substring-after(@uri,$path)"/>
+         <xhtml:span class="global">
+	    <xsl:value-of select="substring-after(@uri,$path)"/>
+         </xhtml:span>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template name="uri">
+   <xsl:variable name="url">
+      <xsl:call-template name="lddlurl"/>
+      <xsl:value-of select="substring-after(@uri,'ld:')"/>
+      <xsl:text>.html</xsl:text>
+   </xsl:variable>
+   <rlink to="{$url}"><xsl:value-of select="@name"/></rlink>
+</xsl:template>
+
+<xsl:template name="layer">
+   <xhtml:sup>
+      <xsl:choose>
+         <xsl:when test="@layer">
+            <xsl:value-of select="@layer"/>
+         </xsl:when>
+         <xsl:otherwise>
+            <xsl:call-template name="infinity"/>
+         </xsl:otherwise>
+      </xsl:choose>
+   </xhtml:sup>
+</xsl:template>
+
+<xsl:template name="abst">
+   <xsl:choose>
+      <xsl:when test="@layer=0 and @position=1">
+	 <xsl:call-template name="forall"/>
+         <xsl:call-template name="layer"/>
+      </xsl:when>
+      <xsl:when test="@layer=0">
+	 <xsl:call-template name="Pi"/>
+         <xsl:call-template name="layer"/>
+      </xsl:when>
+      <xsl:when test="@layer=1 and @position=1">
+	 <xsl:call-template name="forall"/>
+      </xsl:when>
+      <xsl:when test="@layer=1">
+	 <xsl:call-template name="Pi"/>
+      </xsl:when>
+      <xsl:when test="@layer=2">
+         <xsl:call-template name="lambda"/>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:call-template name="lambda"/>
+         <xsl:call-template name="layer"/>
       </xsl:otherwise>
    </xsl:choose>
 </xsl:template>
 
-<xsl:template name="lddl">
-   <xsl:text disable-output-escaping="yes">&amp;lambda;&amp;delta; Digital Library (LDDL)</xsl:text>
+<xsl:template name="abbr">
+   <xsl:call-template name="delta"/>
+</xsl:template>
+
+<xsl:template name="void">
+   <xsl:call-template name="chi"/>
 </xsl:template>
 
+<xsl:template name="name">
+   <xsl:choose>
+      <xsl:when test="@name">
+         <xsl:value-of select="@name"/>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:call-template name="us"/>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template name="separator">
+
+<!--
+   <xsl:variable name="pos">
+      <xsl:value-of select="position()"/>
+   </xsl:variable>
+   <xsl:variable name="last">
+      <xsl:value-of select="last()"/>
+   </xsl:variable>
+   <xhtml:span class="separator" title="{$pos} {$last}">
+      <xsl:call-template name="fs"/>
+   </xhtml:span>
+-->
+   <xsl:choose>
+      <xsl:when test="last()>position()">
+         <xhtml:span class="separator">
+            <xsl:call-template name="fs"/>
+         </xhtml:span>
+      </xsl:when>
+   </xsl:choose>
+</xsl:template>
+
+<!--
+
+<xsl:template name="multiple">
+   <xhtml:span class="separator">
+      <xsl:call-template name="cm"/>
+   </xhtml:span>
+</xsl:template>
+
+<xsl:template name="mk_terms">
+   <xsl:for-each select="*">
+      <xsl:apply-templates select="."/>
+      <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
+         <xsl:call-template name="multiple"/>
+      </xsl:if>
+   </xsl:for-each>
+</xsl:template>
+
+-->
+
 </xsl:stylesheet>