From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 12 Sep 2011 12:00:49 +0000 (+0000)
Subject: refactoring completed!
X-Git-Tag: make_still_working~2288
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eadeb433386822aac6862c76ba73957c07a99098;p=helm.git

refactoring completed!
---

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 248d12606..9070d13c4 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -10,29 +10,17 @@ KEEP = README
 
 CLEAN = etc/log.txt etc/profile.txt
 
-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
+TAGS = test-si test-si-fast profile xml-si xml-si-crg 
 
 include Makefile.common
 
+XMLDIR  = $(HOME)/svn/helm-stable/www/lambda_delta
+
 INPUT = examples/grundlagen/grundlagen.aut
 
 test-si: $(MAIN).opt etc
 	@echo "  HELENA -p -o -c $(INPUT)"
-	$(H)./$(MAIN).opt -p -o -c -S 3 $(O) $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -p -o -c -S 3 -O $(XMLDIR) $(O) $(INPUT) > etc/log.txt
 
 test-si-fast: $(MAIN).opt etc
 	@echo "  HELENA -o -q $(INPUT)"
@@ -46,55 +34,8 @@ profile: $(MAIN).opt etc
 
 xml-si: $(MAIN).opt etc
 	@echo "  HELENA -o -x -s 2 $(INPUT)"
-	$(H)./$(MAIN).opt -o -x -s 2 -S 1 $(INPUT) > etc/log.txt
+	$(H)./$(MAIN).opt -o -x -s 2 -S 1 -O $(XMLDIR) $(INPUT) > etc/log.txt
 
 xml-si-crg: $(MAIN).opt etc
 	@echo "  HELENA -o -x -s 1 $(INPUT)"
-	$(H)./$(MAIN).opt -o -x -s 1 -S 1 $(INPUT) > etc/log.txt
-
-etc:
-	@echo "  MKDIR etc"
-	$(H)mkdir etc
-
-%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
-
-%.ld:
-	@echo "  XSLT $@"
-	$(H)mkdir -p $(LOCALLDDLDIR)/$(@D)
-	$(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/lddl.xsl xml/$@.xml
-
-%.ldc:
-	@echo "  SKIP $@"
-
-etc/make-html.sh xml/index.txt index:
-	@echo "  GENERATE INDEXES"
-	$(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt
-	$(H)sed "s/^/make --no-print-directory /" xml/index.txt | sed s.ld:/.. > etc/make-html.sh
-
-html: etc/make-html.sh
-	@echo "  MAKE */*.ld"
-	$(H). $<
-
-test-html:
-	@$(MAKE) --no-print-directory $(XMLS:xml/%.xml=%)
-
-install-html: etc/make-html.sh
-	@echo "  INSTALL xml"
-	$(H)scp -r $(LOCALLDDLDIR)/* $(LDDLDIR)
-
-install-lddl: index
-	@echo "  INSTALL lddl.tar.bz2"
-	$(H)tar -cjf etc/lddl.tar.bz2 -X etc/exclude.txt xml
-	$(H)scp etc/lddl.tar.bz2 $(DOWNDIR)
-
-install-dtd: xml/ld.dtd
-	@echo "  INSTALL $<"
-	$(H)scp $< $(XMLDIR)
-
-install-css: xml/ld-html.css
-	@echo "  INSTALL $<"
-	$(H)scp $< $(LDDLDIR)
-
-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)
+	$(H)./$(MAIN).opt -o -x -s 1 -S 1 -O $(XMLDIR) $(INPUT) > etc/log.txt
diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common
index 00c54f873..902f37a3d 100644
--- a/helm/software/helena/Makefile.common
+++ b/helm/software/helena/Makefile.common
@@ -7,11 +7,7 @@ endif
 
 RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
 
-LDDLURL = http://lambda-delta.info/static/lddl
-LDDLDIR = mowgli:/projects/helm/public_html/lambda-delta/static/lddl
 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))
 
@@ -21,8 +17,6 @@ OCAMLDEP  = $(OCAMLFIND) ocamldep -native $(INCLUDES)
 OCAMLOPT  = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES)
 OCAMLLEX  = ocamllex.opt
 OCAMLYACC = ocamlyacc -v
-XMLLINT   = xmllint --noout
-XSLT      = xsltproc
 TAR       = tar -czf etc/$(MAIN:%=%.tgz)
 
 define DIR_TEMPLATE
@@ -69,10 +63,6 @@ clean:
 	@echo "  CLEAN . $(SRC)"
 	$(H)find -name "*~" | xargs $(RM) $(CLEAN)
 
-lint-xml: $(XMLS)
-	@echo XMLLINT --valid
-	$(H)$(XMLLINT) --valid $^ 
-
 relise: clean
 	@echo "  RELISE $(RELISE)"
 	$(H)mkdir -p $(RELISE)
@@ -84,6 +74,10 @@ tgz: clean
 	@echo "  TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" 
 	$(H)find -name "Make*" | xargs $(TAR) $(KEEP)
 
+etc:
+	@echo "  MKDIR etc"
+	$(H)mkdir etc
+
 %.ml %.mli: %.mly
 	@echo "  OCAMLYACC $<"
 	$(H)$(OCAMLYACC) $<
diff --git a/helm/software/helena/xml/ld.css b/helm/software/helena/xml/ld.css
deleted file mode 100644
index 92d2e8d92..000000000
--- a/helm/software/helena/xml/ld.css
+++ /dev/null
@@ -1,63 +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 */
-}
diff --git a/helm/software/helena/xml/ld.dtd b/helm/software/helena/xml/ld.dtd
deleted file mode 100644
index 3dd881315..000000000
--- a/helm/software/helena/xml/ld.dtd
+++ /dev/null
@@ -1,140 +0,0 @@
-<?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/software/helena/xml/lddl.css b/helm/software/helena/xml/lddl.css
deleted file mode 100644
index 41a635d45..000000000
--- a/helm/software/helena/xml/lddl.css
+++ /dev/null
@@ -1,43 +0,0 @@
-@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
deleted file mode 100644
index 2711cff96..000000000
--- a/helm/software/helena/xml/lddl.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="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
deleted file mode 100644
index 676d37722..000000000
--- a/helm/software/helena/xml/lddl_entry.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/lddl_library.xsl b/helm/software/helena/xml/lddl_library.xsl
deleted file mode 100644
index c7914ed64..000000000
--- a/helm/software/helena/xml/lddl_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/lddl_root.xsl b/helm/software/helena/xml/lddl_root.xsl
deleted file mode 100644
index c4cf27cd8..000000000
--- a/helm/software/helena/xml/lddl_root.xsl
+++ /dev/null
@@ -1,113 +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/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
deleted file mode 100644
index 4e0c488b5..000000000
--- a/helm/software/helena/xml/lddl_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>