From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 Sep 2011 14:03:37 +0000 (+0000)
Subject: the refactoring continues ...
X-Git-Tag: make_still_working~2292
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=354731c43c5d5b8d050564025e26fdc3bc85acb9;p=helm.git

the refactoring continues ...
---

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index d8aa348f4..248d12606 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -14,24 +14,22 @@ TAGS = test-si test-si-fast profile xml-si xml-si-crg html test-html \
        install-html install-lddl install-dtd install-xml instal-css
 
 
-XMLS = xml/brg-si/grundlagen/l/not.ld.xml \
-       xml/brg-si/grundlagen/l/et.ld.xml \
-       xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
-       xml/brg-si/grundlagen/l/e/pairis1.ld.xml \
-       xml/brg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
-       xml/crg-si/grundlagen/l/not.ld.xml \
-       xml/crg-si/grundlagen/l/et.ld.xml \
-       xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
-       xml/crg-si/grundlagen/l/e/pairis1.ld.xml \
-       xml/crg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
-       xml/brg-si/grundlagen/ccs.ldc.xml
+XMLS = xml/brg_si/grundlagen/l/not.ld.xml \
+       xml/brg_si/grundlagen/l/et.ld.xml \
+       xml/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+       xml/brg_si/grundlagen/l/e/pairis1.ld.xml \
+       xml/brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+       xml/crg_si/grundlagen/l/not.ld.xml \
+       xml/crg_si/grundlagen/l/et.ld.xml \
+       xml/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+       xml/crg_si/grundlagen/l/e/pairis1.ld.xml \
+       xml/crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+       xml/brg_si/grundlagen/ccs.ldc.xml
 
 include Makefile.common
 
 INPUT = examples/grundlagen/grundlagen.aut
 
-SLS = helena.sl automath.sl
-
 test-si: $(MAIN).opt etc
 	@echo "  HELENA -p -o -c $(INPUT)"
 	$(H)./$(MAIN).opt -p -o -c -S 3 $(O) $(INPUT) > etc/log.txt
@@ -63,7 +61,7 @@ etc:
 %.ld:
 	@echo "  XSLT $@"
 	$(H)mkdir -p $(LOCALLDDLDIR)/$(@D)
-	$(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml
+	$(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/lddl.xsl xml/$@.xml
 
 %.ldc:
 	@echo "  SKIP $@"
@@ -99,12 +97,4 @@ install-css: xml/ld-html.css
 
 install-xml: etc/make-html.sh
 	@echo "  INSTALL xml"
-	$(H)scp -r xml/index.txt xml/ld.dtd xml/brg-si/ xml/crg-si/ $(XMLDIR)
-
-install-icons:
-	@echo "  INSTALL *.png *.ico"
-	$(H)scp icons/*.png icons/*.ico $(DOWNDIR)
-
-install-jed:
-	@echo "  INSTALL $(SLS)"
-	$(H)scp $(SLS:%=$(HOME)/jed/%) $(DOWNDIR)
+	$(H)scp -r xml/index.txt xml/ld.dtd xml/brg_si/ xml/crg_si/ $(XMLDIR)
diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common
index 80019a800..00c54f873 100644
--- a/helm/software/helena/Makefile.common
+++ b/helm/software/helena/Makefile.common
@@ -1,6 +1,6 @@
 H=@
 ifeq ($(origin OCAMLPATH), undefined)
-   OCAMLFIND = OCAMLPATH=$(HOME)/svn/software/components/METAS ocamlfind
+   OCAMLFIND = OCAMLPATH=$(HOME)/svn/helm-stable/software/components/METAS ocamlfind
 else
    OCAMLFIND = ocamlfind
 endif
@@ -9,8 +9,8 @@ RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
 
 LDDLURL = http://lambda-delta.info/static/lddl
 LDDLDIR = mowgli:/projects/helm/public_html/lambda-delta/static/lddl
-DOWNDIR = mowgli:/projects/helm/public_html/lambda-delta/download
-XMLDIR  = mowgli:/projects/helm/public_html/lambda-delta/xml
+DOWNDIR = $(HOME)/svn/helm-stable/www/lambda_delta/download
+XMLDIR  = mowgli:/projects/helm/public_html/lambda_delta/xml
 LOCALLDDLDIR = $(HOME)/public_html/lddl
 
 DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make))
diff --git a/helm/software/helena/icons/b3.png b/helm/software/helena/icons/b3.png
deleted file mode 100644
index 3ed538923..000000000
Binary files a/helm/software/helena/icons/b3.png and /dev/null differ
diff --git a/helm/software/helena/icons/b4.png b/helm/software/helena/icons/b4.png
deleted file mode 100644
index ccfd1a99a..000000000
Binary files a/helm/software/helena/icons/b4.png and /dev/null differ
diff --git a/helm/software/helena/icons/b5.png b/helm/software/helena/icons/b5.png
deleted file mode 100644
index 30cace1d1..000000000
Binary files a/helm/software/helena/icons/b5.png and /dev/null differ
diff --git a/helm/software/helena/icons/b9.png b/helm/software/helena/icons/b9.png
deleted file mode 100644
index 0de559867..000000000
Binary files a/helm/software/helena/icons/b9.png and /dev/null differ
diff --git a/helm/software/helena/icons/basic-32.png b/helm/software/helena/icons/basic-32.png
deleted file mode 100644
index 350f6bcb0..000000000
Binary files a/helm/software/helena/icons/basic-32.png and /dev/null differ
diff --git a/helm/software/helena/icons/crux-16.ico b/helm/software/helena/icons/crux-16.ico
deleted file mode 100644
index 7323c8af8..000000000
Binary files a/helm/software/helena/icons/crux-16.ico and /dev/null differ
diff --git a/helm/software/helena/icons/crux-32.png b/helm/software/helena/icons/crux-32.png
deleted file mode 100644
index be5524e5e..000000000
Binary files a/helm/software/helena/icons/crux-32.png and /dev/null differ
diff --git a/helm/software/helena/icons/helena-32.png b/helm/software/helena/icons/helena-32.png
deleted file mode 100644
index 4a065aefe..000000000
Binary files a/helm/software/helena/icons/helena-32.png and /dev/null differ
diff --git a/helm/software/helena/icons/helena-label.png b/helm/software/helena/icons/helena-label.png
deleted file mode 100644
index 55487ab99..000000000
Binary files a/helm/software/helena/icons/helena-label.png and /dev/null differ
diff --git a/helm/software/helena/icons/rainbow.png b/helm/software/helena/icons/rainbow.png
deleted file mode 100644
index 45925baa7..000000000
Binary files a/helm/software/helena/icons/rainbow.png and /dev/null differ
diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index c133bed7c..8cc200ad9 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -45,7 +45,7 @@ let kernel_id () =
       | Brg -> "brg"
       | Bag -> "bag"
    in
-   let si = if !si then "-si" else "" in
+   let si = if !si then "_si" else "" in
    id ^ si
 
 let get_baseuri () =
diff --git a/helm/software/helena/xml/ld-html-entity.xsl b/helm/software/helena/xml/ld-html-entity.xsl
deleted file mode 100644
index 676d37722..000000000
--- a/helm/software/helena/xml/ld-html-entity.xsl
+++ /dev/null
@@ -1,61 +0,0 @@
-<?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/software/helena/xml/ld-html-library.xsl b/helm/software/helena/xml/ld-html-library.xsl
deleted file mode 100644
index c7914ed64..000000000
--- a/helm/software/helena/xml/ld-html-library.xsl
+++ /dev/null
@@ -1,283 +0,0 @@
-<?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/software/helena/xml/ld-html-root.xsl b/helm/software/helena/xml/ld-html-root.xsl
deleted file mode 100644
index 72958381b..000000000
--- a/helm/software/helena/xml/ld-html-root.xsl
+++ /dev/null
@@ -1,110 +0,0 @@
-<?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/static/lddl/ld-html.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://www.cs.unibo.it/%7Efguidi/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/software/helena/xml/ld-html-term.xsl b/helm/software/helena/xml/ld-html-term.xsl
deleted file mode 100644
index 4e0c488b5..000000000
--- a/helm/software/helena/xml/ld-html-term.xsl
+++ /dev/null
@@ -1,96 +0,0 @@
-<?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>
diff --git a/helm/software/helena/xml/ld-html.css b/helm/software/helena/xml/ld-html.css
deleted file mode 100644
index 705e15993..000000000
--- a/helm/software/helena/xml/ld-html.css
+++ /dev/null
@@ -1,105 +0,0 @@
-@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 */
-}
-
-/* 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/software/helena/xml/ld-html.xsl b/helm/software/helena/xml/ld-html.xsl
deleted file mode 100644
index d21a6bbf9..000000000
--- a/helm/software/helena/xml/ld-html.xsl
+++ /dev/null
@@ -1,33 +0,0 @@
-<?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="ld-html-library.xsl"/>
-<xsl:include href="ld-html-term.xsl"/>
-<xsl:include href="ld-html-entity.xsl"/>
-<xsl:include href="ld-html-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/software/helena/xml/ld.css b/helm/software/helena/xml/ld.css
new file mode 100644
index 000000000..92d2e8d92
--- /dev/null
+++ b/helm/software/helena/xml/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/software/helena/xml/ld.dtd b/helm/software/helena/xml/ld.dtd
index 3939d6f5b..3dd881315 100644
--- a/helm/software/helena/xml/ld.dtd
+++ b/helm/software/helena/xml/ld.dtd
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 
-<!-- DTD for persistent lambda-delta logical data -->
+<!-- DTD for persistent lambda_delta logical data -->
 
 <!-- TERMS -->
 
@@ -103,7 +103,7 @@
 
 <!ELEMENT ENTITY %entity;>
 <!ATTLIST ENTITY
-          xmlns     CDATA    #FIXED    "http://lambda-delta.info"
+          xmlns     CDATA    #FIXED    "http://lambda_delta.info"
 	  hierarchy NMTOKEN  #REQUIRED
           options   NMTOKENS #IMPLIED
 >
@@ -135,6 +135,6 @@
 
 <!ELEMENT CCS %ccs;>
 <!ATTLIST CCS
-          xmlns CDATA #FIXED    "http://lambda-delta.info"
+          xmlns CDATA #FIXED    "http://lambda_delta.info"
           uri   CDATA #REQUIRED
 >
diff --git a/helm/software/helena/xml/lddl.css b/helm/software/helena/xml/lddl.css
new file mode 100644
index 000000000..41a635d45
--- /dev/null
+++ b/helm/software/helena/xml/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/software/helena/xml/lddl.xsl b/helm/software/helena/xml/lddl.xsl
new file mode 100644
index 000000000..2711cff96
--- /dev/null
+++ b/helm/software/helena/xml/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/software/helena/xml/lddl_entry.xsl b/helm/software/helena/xml/lddl_entry.xsl
new file mode 100644
index 000000000..676d37722
--- /dev/null
+++ b/helm/software/helena/xml/lddl_entry.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/software/helena/xml/lddl_library.xsl b/helm/software/helena/xml/lddl_library.xsl
new file mode 100644
index 000000000..c7914ed64
--- /dev/null
+++ b/helm/software/helena/xml/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/software/helena/xml/lddl_root.xsl b/helm/software/helena/xml/lddl_root.xsl
new file mode 100644
index 000000000..c4cf27cd8
--- /dev/null
+++ b/helm/software/helena/xml/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/software/helena/xml/lddl_term.xsl b/helm/software/helena/xml/lddl_term.xsl
new file mode 100644
index 000000000..4e0c488b5
--- /dev/null
+++ b/helm/software/helena/xml/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>