From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 Sep 2011 18:51:41 +0000 (+0000)
Subject: refactoring and regeneration of lddl
X-Git-Tag: make_still_working~2291
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae47e671a2e5b1c6498e62e0fd8703cea7ba53b2;p=helm.git

refactoring and regeneration of lddl
---

diff --git a/helm/www/lambda_delta/Makefile b/helm/www/lambda_delta/Makefile
new file mode 100644
index 000000000..34eacbeb8
--- /dev/null
+++ b/helm/www/lambda_delta/Makefile
@@ -0,0 +1,83 @@
+H=@
+
+TAGS = lint-xml index lddl install-xml \
+       test-html html install-html \
+       install-jed install-bib
+
+LDDLURL = http://lambda-delta.info/static/lddl
+
+ETCDIR   = etc
+DOWNDIR  = download
+XSLTDIR  = xslt
+XMLDIR   = xml
+HTMLDIR  = $(HOME)/public_html/lddl
+JEDDIR   = $(HOME)/mps/jed
+BIBDIR   = $(HOME)/texmf/bibtex/bib
+
+RXMLDIR  = helm:/projects/helm/public_html/lambda_delta/xml
+RHTMLDIR = helm:/projects/helm/public_html/lambda_delta/static/lddl
+
+SLS = helena.sl automath.sl
+BIB = lambda_delta.bib
+
+XMLS = brg_si/grundlagen/l/not.ld.xml \
+       brg_si/grundlagen/l/et.ld.xml \
+       brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+       brg_si/grundlagen/l/e/pairis1.ld.xml \
+       brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+       crg_si/grundlagen/l/not.ld.xml \
+       crg_si/grundlagen/l/et.ld.xml \
+       crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+       crg_si/grundlagen/l/e/pairis1.ld.xml \
+       crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+       brg_si/grundlagen/ccs.ldc.xml
+
+XMLLINT = xmllint --noout
+XSLT    = xsltproc
+
+lint-xml: $(XMLS:%=$(XMLDIR)/%)
+	@echo XMLLINT --valid
+	$(H)$(XMLLINT) --valid $^ 
+
+$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index:
+	@echo "  GENERATE INDEXES"
+	$(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt
+	$(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh
+
+lddl: $(ETCDIR)/exclude.txt index
+	@echo "  GENERATE lddl.tar.bz2"
+	$(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) 
+
+install-xml: $(XMLDIR)/index.txt
+	@echo "  INSTALL xml"
+	$(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR)
+
+test-html:
+	@$(MAKE) --no-print-directory $(XMLS:%.xml=%)
+
+html: $(ETCDIR)/make-html.sh
+	@echo "  MAKE */*.ld"
+	$(H). $<
+
+install-html: $(ETCDIR)/make_html.sh
+	@echo "  INSTALL html"
+	$(H)scp -r $(HTMLDIR)/* $(RHTMLDIR)
+
+install-jed: $(SLS:%=$(JEDDIR)/%)
+	@echo "  INSTALL $(SLS)"
+	$(H)scp $(SLS:%=$(JEDDIR)/%) $(DOWNDIR)
+
+install-bib: $(BIB:%=$(BIBDIR)/%)
+	@echo "  INSTALL $(BIB)"
+	$(H)scp $< $(DOWNDIR)
+	$(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt)
+
+%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
+
+%.ld:
+	@echo "  XSLT $@"
+	$(H)mkdir -p $(HTMLDIR)/$(@D)
+	$(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml
+
+%.ldc:
+	@echo "  SKIP $@"
diff --git a/helm/www/lambda_delta/css/ld.css b/helm/www/lambda_delta/css/ld.css
new file mode 100644
index 000000000..92d2e8d92
--- /dev/null
+++ b/helm/www/lambda_delta/css/ld.css
@@ -0,0 +1,63 @@
+@charset "UTF-8";
+
+/* general ******************************************************************/
+
+body {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 0);
+   margin: 2.5%;
+}
+
+a:link, a:visited {
+   text-decoration: underline;
+}
+
+a:active, a:hover, a:focus {
+   background: rgb(192, 192, 192);
+}
+
+/* blocks *******************************************************************/
+
+.spacer {
+   text-align: center;
+}
+
+.head1 {
+   margin: 0.5em 0; 
+   text-align: center;
+   font-weight: bold; 
+   font-size: xx-large;
+}
+
+.head2 {
+   margin: 0.5em 0; 
+   text-align: left;
+   font-weight: bold; 
+   font-size: x-large;
+}
+
+.text {
+   margin: 1em 0; 
+   text-align: left;
+}
+
+/* inline decorations *******************************************************/
+
+.icon32 {
+   border: 0; 
+   width: 32px; 
+   height: 32px;
+}
+
+.rule {
+   border: 0; 
+   height: 4px;
+   width: 100%; 
+}
+
+.w3c {
+   margin: 0 0.5em; 
+   border: 0; 
+   width: 88px; 
+   height: 32px; /* this should be 31px */
+}
diff --git a/helm/www/lambda_delta/css/lddl.css b/helm/www/lambda_delta/css/lddl.css
new file mode 100644
index 000000000..41a635d45
--- /dev/null
+++ b/helm/www/lambda_delta/css/lddl.css
@@ -0,0 +1,43 @@
+@charset "UTF-8";
+
+/* terms ********************************************************************/
+
+.separator {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 0);
+}
+
+.sort {
+   background: rgb(255, 255, 255); 
+   color: rgb(128, 0, 255);
+}
+
+.lref {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 0);
+}
+
+.gref {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 255);
+}
+
+.appl {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 0);
+}
+
+.cast {
+   background: rgb(255, 255, 255); 
+   color: rgb(255, 0, 0);
+}
+
+.local {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 160, 0);
+}
+
+.global {
+   background: rgb(255, 255, 255); 
+   color: rgb(0, 0, 0);
+}
diff --git a/helm/www/lambda_delta/download/lambda_delta.bib b/helm/www/lambda_delta/download/lambda_delta.bib
index 26c994a96..f6df7f861 100644
--- a/helm/www/lambda_delta/download/lambda_delta.bib
+++ b/helm/www/lambda_delta/download/lambda_delta.bib
@@ -70,9 +70,9 @@
 
 @misc{lambdadelta1,
    author="F. {Guidi}",
-   title="{lambda-delta}",
-   howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1",
+   title="{lambda\_delta\_1}",
+   howpublished="Formal specification with the proof assistant Coq 7.3.1",
    year="2007",
    month="January",
-   note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}"
+   note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
 }
diff --git a/helm/www/lambda_delta/download/lambda_delta.txt b/helm/www/lambda_delta/download/lambda_delta.txt
index 26c994a96..f6df7f861 100644
--- a/helm/www/lambda_delta/download/lambda_delta.txt
+++ b/helm/www/lambda_delta/download/lambda_delta.txt
@@ -70,9 +70,9 @@
 
 @misc{lambdadelta1,
    author="F. {Guidi}",
-   title="{lambda-delta}",
-   howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1",
+   title="{lambda\_delta\_1}",
+   howpublished="Formal specification with the proof assistant Coq 7.3.1",
    year="2007",
    month="January",
-   note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}"
+   note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
 }
diff --git a/helm/www/lambda_delta/download/lddl.tar.bz2 b/helm/www/lambda_delta/download/lddl.tar.bz2
index 853e7a907..8033d3784 100644
Binary files a/helm/www/lambda_delta/download/lddl.tar.bz2 and b/helm/www/lambda_delta/download/lddl.tar.bz2 differ
diff --git a/helm/www/lambda_delta/xml/ld.dtd b/helm/www/lambda_delta/xml/ld.dtd
new file mode 100644
index 000000000..3dd881315
--- /dev/null
+++ b/helm/www/lambda_delta/xml/ld.dtd
@@ -0,0 +1,140 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for persistent lambda_delta logical data -->
+
+<!-- TERMS -->
+
+<!ENTITY % leaf '(Sort|LRef|GRef)'>
+
+<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+
+<!ENTITY % term '(%node;*,%leaf;)'>
+
+<!ENTITY % terms '(%term;*)'>
+
+<!ELEMENT Sort EMPTY>
+<!ATTLIST Sort
+          position NMTOKEN #REQUIRED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+	  meta     CDATA   #IMPLIED
+>
+
+<!ELEMENT LRef EMPTY>
+<!ATTLIST LRef
+          position NMTOKEN #REQUIRED
+	  offset   NMTOKEN #IMPLIED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+	  meta     CDATA   #IMPLIED
+>
+
+<!ELEMENT GRef EMPTY>
+<!ATTLIST GRef
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+	  meta CDATA   #IMPLIED
+>
+
+<!ELEMENT Cast %term;>
+<!ATTLIST Cast
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
+>
+
+<!ELEMENT Appl %terms;>
+<!ATTLIST Appl
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
+>
+
+<!ELEMENT Abst %terms;>
+<!ATTLIST Abst
+          level NMTOKEN  #IMPLIED
+	  name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
+>
+
+<!ELEMENT Abbr %terms;>
+<!ATTLIST Abbr
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
+>
+
+<!ELEMENT Void EMPTY>
+<!ATTLIST Void
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+	  mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
+>
+
+<!-- ENVIRONMENT ENTRIES -->
+
+<!ENTITY % entity '(ABST|ABBR)'> 
+
+<!ELEMENT ABST %term;>
+<!ATTLIST ABST
+          uri   CDATA    #REQUIRED
+          level NMTOKEN  #IMPLIED
+          name  NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  NMTOKENS #IMPLIED
+	  lang  NMTOKEN  "en-US"
+	  info  CDATA    #IMPLIED
+>
+
+<!ELEMENT ABBR %term;>
+<!ATTLIST ABBR
+          uri  CDATA    #REQUIRED
+          name NMTOKEN  #IMPLIED
+          mark NMTOKEN  #IMPLIED
+	  meta NMTOKENS #IMPLIED
+	  lang NMTOKEN  "en-US"
+	  info CDATA    #IMPLIED
+>
+
+<!ELEMENT ENTITY %entity;>
+<!ATTLIST ENTITY
+          xmlns     CDATA    #FIXED    "http://lambda_delta.info"
+	  hierarchy NMTOKEN  #REQUIRED
+          options   NMTOKENS #IMPLIED
+>
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % cc '(ToPositive|ToOne|ToNext)'> 
+
+<!ENTITY % ccs '(%cc;*)'>
+
+<!ELEMENT ToPositive EMPTY>
+<!ATTLIST ToPositive
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToOne EMPTY>
+<!ATTLIST ToOne
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToNext EMPTY>
+<!ATTLIST ToNext
+          arity NMTOKEN  #IMPLIED
+          prec  NMTOKENS #IMPLIED
+          next  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+          xmlns CDATA #FIXED    "http://lambda_delta.info"
+          uri   CDATA #REQUIRED
+>
diff --git a/helm/www/lambda_delta/xslt/lddl.xsl b/helm/www/lambda_delta/xslt/lddl.xsl
new file mode 100644
index 000000000..2711cff96
--- /dev/null
+++ b/helm/www/lambda_delta/xslt/lddl.xsl
@@ -0,0 +1,33 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:param name="baseurl"/>
+
+<xsl:include href="lddl_library.xsl"/>
+<xsl:include href="lddl_term.xsl"/>
+<xsl:include href="lddl_entity.xsl"/>
+<xsl:include href="lddl_root.xsl"/>
+
+<xsl:output 
+   method="xml"
+   doctype-public="-//W3C//DTD XHTML 1.1//EN"
+   doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"   
+   encoding="UTF-8"
+   indent="no"
+/>
+
+</xsl:stylesheet>
diff --git a/helm/www/lambda_delta/xslt/lddl_entity.xsl b/helm/www/lambda_delta/xslt/lddl_entity.xsl
new file mode 100644
index 000000000..676d37722
--- /dev/null
+++ b/helm/www/lambda_delta/xslt/lddl_entity.xsl
@@ -0,0 +1,61 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ABST ABBR"/>
+
+<xsl:template name="ENTITY">
+   <xsl:param name="kind"/>
+   <div class="head2">
+      <span class="global">
+         <xsl:value-of select="$kind"/>
+         <xsl:call-template name="cn"/>
+         <xsl:call-template name="sp"/>
+         <span class="gref">   
+            <xsl:call-template name="global"/>
+         </span>
+         <xsl:call-template name="sp"/>
+         <xsl:call-template name="op"/>
+         <span class="gref">
+            <xsl:call-template name="mk_path"/>
+         </span>
+         <xsl:call-template name="cp"/>
+      </span>      
+   </div>
+   <div class="text">
+      <xsl:call-template name="idescr"/>
+      <xsl:call-template name="qt"/>
+      <xsl:value-of select="@meta"/>
+      <xsl:call-template name="qt"/>
+   </div>
+   <div class="text">
+      <xsl:apply-templates/>
+   </div>
+</xsl:template>
+
+<xsl:template match="ABST">
+   <xsl:call-template name="ENTITY">
+      <xsl:with-param name="kind">Declaration</xsl:with-param>
+   </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="ABBR">
+   <xsl:call-template name="ENTITY">
+      <xsl:with-param name="kind">Definition</xsl:with-param>
+   </xsl:call-template>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/www/lambda_delta/xslt/lddl_library.xsl b/helm/www/lambda_delta/xslt/lddl_library.xsl
new file mode 100644
index 000000000..c7914ed64
--- /dev/null
+++ b/helm/www/lambda_delta/xslt/lddl_library.xsl
@@ -0,0 +1,283 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns="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>
+
+<xsl:template name="op">
+   <xsl:text>(</xsl:text>
+</xsl:template>
+
+<xsl:template name="cp">
+   <xsl:text>)</xsl:text>
+</xsl:template>
+
+<xsl:template name="ob">
+   <xsl:text>[</xsl:text>
+</xsl:template>
+
+<xsl:template name="cb">
+   <xsl:text>]</xsl:text>
+</xsl:template>
+
+<xsl:template name="oa">
+   <xsl:text>&lt;</xsl:text>
+</xsl:template>
+
+<xsl:template name="ca">
+   <xsl:text>&gt;</xsl:text>
+</xsl:template>
+
+<xsl:template name="cn">
+   <xsl:text>:</xsl:text>
+</xsl:template>
+
+<xsl:template name="eq">
+   <xsl:text>=</xsl:text>
+</xsl:template>
+
+<xsl:template name="qt">
+   <xsl:text>"</xsl:text>
+</xsl:template>
+
+<xsl:template name="idescr">
+   <xsl:text>Informal description: </xsl:text>
+</xsl:template>
+
+<xsl:template name="vpars">
+   <xsl:text>Validation parameters: </xsl:text>
+</xsl:template>
+
+<xsl:template name="shier">
+   <xsl:text>sort hierarchy = </xsl:text>
+</xsl:template>
+
+<xsl:template name="kopts">
+   <xsl:text>kernel options = </xsl:text>
+</xsl:template>
+
+<xsl:template name="multiple">
+   <span class="separator">
+      <xsl:call-template name="cm"/>
+   </span>
+</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>
+
+<xsl:template name="delta">
+   <a title="{@mark}">
+      <xsl:text disable-output-escaping="yes">&amp;delta;</xsl:text>
+   </a>
+</xsl:template>
+
+<xsl:template name="chi">
+   <a title="{@mark}">
+      <xsl:text disable-output-escaping="yes">&amp;chi;</xsl:text>
+   </a>
+</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>
+
+<xsl:template name="uri">
+   <xsl:variable name="url">
+      <xsl:value-of select="$baseurl"/>
+      <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>
+
+<xsl:template name="global">
+   <a title="{@mark}">
+      <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>
+</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>
+
+<xsl:template name="mk_segment">
+   <xsl:param name="path"/>
+   <xsl:param name="name"/>
+   <xsl:variable name="url">
+      <xsl:value-of select="$baseurl"/>
+      <xsl:value-of select="substring-after($path,'ld:')"/>
+   </xsl:variable>
+   <a href="{$url}"><xsl:value-of select="$name"/></a>
+   <xsl:call-template name="sl"/>
+</xsl:template>
+
+<xsl:template name="mk_path">
+   <xsl:param name="rpath" select="@uri"/>
+   <xsl:variable name="newrpath" select="substring-after($rpath,'/')"/>
+   <xsl:choose>
+      <xsl:when test="$newrpath">
+         <xsl:variable name="segment" select="substring-before($rpath,$newrpath)"/>
+         <xsl:call-template name="mk_segment">
+            <xsl:with-param name="path" select="substring-before(@uri,$newrpath)"/>
+            <xsl:with-param name="name" select="substring-before($segment,'/')"/>
+         </xsl:call-template>
+	 <xsl:call-template name="mk_path">
+	    <xsl:with-param name="rpath" select="$newrpath"/>
+	 </xsl:call-template>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
+	 <xsl:value-of select="substring-after(@uri,$path)"/>
+      </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>
+
+</xsl:stylesheet>
diff --git a/helm/www/lambda_delta/xslt/lddl_root.xsl b/helm/www/lambda_delta/xslt/lddl_root.xsl
new file mode 100644
index 000000000..c4cf27cd8
--- /dev/null
+++ b/helm/www/lambda_delta/xslt/lddl_root.xsl
@@ -0,0 +1,113 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ENTITY"/>
+
+<xsl:template match="/">
+   <html xmlns="http://www.w3.org/1999/xhtml"><head>
+      <meta http-equiv="Content-Language" content="en-us"/>
+      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+      <meta http-equiv="Content-Style-Type" content="text/css"/>
+      <meta name="author" content="Ferruccio Guidi"/>
+      <meta name="description" content="lambda_delta digital library"/>
+      <title>lambda_delta digital library (LDDL)</title>
+      <link rel="stylesheet" type="text/css"
+            href="http://lambda-delta.info/css/ld.css"
+      />
+      <link rel="stylesheet" type="text/css"
+            href="http://lambda-delta.info/css/lddl.css"
+      />
+      <link rel="shortcut icon" 
+            href="http://lambda-delta.info/download/crux_16.ico"
+      />
+   </head><body>
+      <div class="spacer">         
+	 <a href="http://lambda-delta.info/">
+         <img class="icon32" 
+	      alt="[lambda_delta home]" title="lambda_delta home"
+	      src="http://lambda-delta.info/download/crux_32.png"
+	 /></a>
+      </div>
+      <div class="head1">	 
+	 <xsl:call-template name="lddl"/>
+      </div>
+      <div class="spacer"> 
+	 <img class="rule"
+	      alt="[Spacer]" title="lambda_delta rainbow rule"
+	      src="http://lambda-delta.info/download/rainbow.png"
+	 />
+      </div>       
+      <xsl:apply-templates/>
+      <div class="spacer">
+         <a href="http://validator.w3.org/check?uri=referer">
+	 <img class="w3c"
+	      alt="[Valid XHTML 1.1]"
+	      title="Valid XHTML 1.1"
+	      src="http://www.w3.org/Icons/valid-xhtml11-blue"
+	 /></a>  
+	 <a href="http://jigsaw.w3.org/css-validator/check/referer">
+         <img class="w3c"
+	      alt="[Valid CSS level 2]"
+	      title="Valid CSS level 2"
+	      src="http://www.w3.org/Icons/valid-css2-blue"
+	 /></a>	 
+	 <a href="http://www.w3.org/XML/">
+         <img class="w3c"
+	      alt="[Generated from XML via XSL]"
+	      title="Generated from XML via XSL"
+	      src="http://lambda-delta.info/download/xml_xsl2.png"
+	 /></a>
+	 <a href="http://lambda-delta.info/implementation.html#helena">
+         <img class="w3c"
+	      alt="[Powered by Helena lambda_delta processor]"
+	      title="Powered by Helena lambda_delta processor"
+	      src="http://lambda-delta.info/download/helena_label.png"
+	 /></a>
+	 <a href="http://www.w3.org/Graphics/PNG/">
+	 <img class="w3c"
+	      alt="[PNG used here]"
+	      title="PNG used here"
+	      src="http://lambda-delta.info/download/PNGnow2.png"
+	 /></a>
+	 <a href="http://www.anybrowser.org/campaign/">
+	 <img class="w3c"
+	      alt="[Viewable with any browser]"
+	      title="Viewable with any browser"
+              src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"
+	 /></a>
+      </div>
+   </body></html>
+</xsl:template>
+
+<xsl:template match="ENTITY">
+   <xsl:apply-templates/>
+   <div class="text">
+      <xsl:call-template name="vpars"/>
+      <xsl:call-template name="shier"/>
+      <xsl:call-template name="qt"/>
+      <xsl:value-of select="@hierarchy"/>
+      <xsl:call-template name="qt"/>
+      <xsl:call-template name="cm"/>
+      <xsl:call-template name="sp"/>
+      <xsl:call-template name="kopts"/>
+      <xsl:call-template name="qt"/>
+      <xsl:value-of select="@options"/>
+      <xsl:call-template name="qt"/>
+   </div>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/www/lambda_delta/xslt/lddl_term.xsl b/helm/www/lambda_delta/xslt/lddl_term.xsl
new file mode 100644
index 000000000..4e0c488b5
--- /dev/null
+++ b/helm/www/lambda_delta/xslt/lddl_term.xsl
@@ -0,0 +1,96 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="Sort LRef GRef Cast Appl Abst Abbr Void"/>
+
+<xsl:template name="separator">
+   <span class="separator">
+      <xsl:call-template name="fs"/>
+   </span>
+</xsl:template>
+
+<xsl:template match="Sort">
+   <span class="sort">
+      <xsl:call-template name="position"/>
+   </span>
+</xsl:template>
+
+<xsl:template match="LRef">
+   <span class="lref">
+      <xsl:call-template name="position"/>
+   </span>
+</xsl:template>
+
+<xsl:template match="GRef">
+   <span class="gref">
+      <xsl:call-template name="uri"/>
+   </span>
+</xsl:template>
+
+<xsl:template match="Cast">
+   <span class="cast">
+      <xsl:call-template name="oa"/>
+      <xsl:apply-templates/>
+      <xsl:call-template name="ca"/>
+   </span>
+   <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Appl">
+   <span class="appl">
+      <xsl:call-template name="op"/>
+      <xsl:call-template name="mk_terms"/>
+      <xsl:call-template name="cp"/>
+   </span>
+   <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Abst">
+   <span class="local">
+      <xsl:call-template name="lambda"/>
+      <xsl:call-template name="mk_binder">
+         <xsl:with-param name="sep-seq">
+            <xsl:call-template name="cn"/>
+         </xsl:with-param>
+      </xsl:call-template>
+   </span>
+   <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Abbr">
+   <span class="local">
+      <xsl:call-template name="delta"/>
+      <xsl:call-template name="mk_binder">
+         <xsl:with-param name="sep-seq">
+            <xsl:call-template name="eq"/>
+         </xsl:with-param>
+      </xsl:call-template>
+   </span>
+   <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Void">
+   <span class="local">
+      <xsl:call-template name="chi"/>
+      <xsl:call-template name="ob"/>
+      <xsl:call-template name="mk_names"/>
+      <xsl:call-template name="cb"/>
+   </span>
+   <xsl:call-template name="separator"/>
+</xsl:template>
+
+</xsl:stylesheet>