From 21e21b3b061807035bbd18d29d7a4fd8086ca10d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 9 Dec 2019 20:38:48 +0100
Subject: [PATCH] grundlagen web pages updated

+ some improvements in XSLT processing
---
 .gitignore                                    |  4 +
 helm/www/lambdadelta/Makefile                 | 10 +-
 helm/www/lambdadelta/css/ld_web.css           | 98 +++++++++----------
 helm/www/lambdadelta/css/lddl.css             | 41 ++++----
 .../web/home/documentation.ldw.xml            |  2 +-
 .../web/home/implementation.ldw.xml           | 10 +-
 helm/www/lambdadelta/xslt/ld_web_root.xsl     | 17 ++--
 helm/www/lambdadelta/xslt/lddl_library.xsl    | 27 +++--
 helm/www/lambdadelta/xslt/lddl_term.xsl       | 38 +++----
 9 files changed, 130 insertions(+), 117 deletions(-)

diff --git a/.gitignore b/.gitignore
index 5958dcdfb..83073d3fc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,6 +45,10 @@ helm/www/lambdadelta/html
 helm/www/lambdadelta/etc/BTM
 helm/www/lambdadelta/etc/lambdadelta
 helm/www/lambdadelta/etc/coq-contribs
+helm/www/lambdadelta/etc/make_html.sh
+helm/www/lambdadelta/web/lddl
+helm/www/lambdadelta/xml/Environment
+helm/www/lambdadelta/xml/index.txt
 helm/www/lambdadelta/xslt/apps_2_src.xsl
 helm/www/lambdadelta/xslt/apps_2_sum.xsl
 helm/www/lambdadelta/xslt/basic_2_blk.xsl
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index 2f35c1365..51ecbd1a5 100644
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -17,7 +17,7 @@ XMLDIR     = xml
 SRCDIR     = web/home
 LDDLDIR    = web/lddl
 XHTBLDIR   = bin/xhtbl
-HTMLDIR    = static/lddl
+HTMLDIR    = html/lddl
 JEDDIR     = $(HOME)/mps/jed
 BIBDIR     = $(HOME)/texmf/bibtex/bib
 CONTRIBDIR = $(ETCDIR)/lambdadelta
@@ -50,7 +50,7 @@ COQ      = coq/grundlagen_2.v
 MATITA = matita/root matita/grundlagen_2.ma
 
 XMLLINT = xmllint --noout
-XSLT    = xalan
+XSLT    = xsltproc
 XHTBL   = $(XHTBLDIR)/xhtbl.native
 
 XHTBLOPTS =
@@ -102,7 +102,7 @@ lint-xml: $(XMLS:%=$(XMLDIR)/%)
 	@echo XMLLINT --valid
 	$(H)$(XMLLINT) --valid $^
 
-$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index:
+$(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
@@ -164,7 +164,7 @@ install-v: $(HELENADIR)/$(COQ)
 
 up-html:
 	@echo "  UPDATE $(RHOMEDIR)/html/"
-	$(H)scp -q -r html $(RHOMEDIR)
+	$(H)scp -q html/*.html $(RHOMEDIR)/html/
 
 up-css:
 	@echo "  UPDATE $(RHOMEDIR)/css/"
@@ -181,7 +181,7 @@ up-download:
 %.ld:
 	@echo "  XSLT $@"
 	$(H)mkdir -p $(LDDLDIR)/$(@D)
-	$(H)$(XSLT) $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
+	$(H)$(XSLT) --novalid $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
 	$(H)mkdir -p $(HTMLDIR)/$(@D)
 	$(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml
 
diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css
index 9f2e42d59..929330851 100644
--- a/helm/www/lambdadelta/css/ld_web.css
+++ b/helm/www/lambdadelta/css/ld_web.css
@@ -3,69 +3,69 @@
 /* general ******************************************************************/
 
 body {
-   background-color: rgb(255, 255, 255); 
-   color: rgb(0, 0, 0);
-   margin: 2.5%;
+  background-color: rgb(255, 255, 255);
+  color: rgb(0, 0, 0);
+  margin: 2.5%;
 }
 
 a:link, a:visited, a:hover, a:active, a:focus {
-   text-decoration: underline;
-   color: inherit;
-   background-color: inherit;
+  text-decoration: underline;
+  color: inherit;
+  background-color: inherit;
 }
 
 a:hover {
-   text-decoration: underline;
-   color: inherit;
-   background-color: rgb(192, 192, 192);
+  text-decoration: underline;
+  color: inherit;
+  background-color: rgb(192, 192, 192);
 }
 
 /* blocks *******************************************************************/
 
 div.spacer {
-   text-align: center;
-   font-weight: normal; 
-   font-size: medium;
+  text-align: center;
+  font-weight: normal;
+  font-size: medium;
 }
 
 div.head1 {
-   margin: 0.5em 0; 
-   text-align: center;
-   font-weight: bold; 
-   font-size: xx-large;
+  margin: 0.5em 0;
+  text-align: center;
+  font-weight: bold;
+  font-size: xx-large;
 }
 
 div.head2sn {
-   margin: 0.5em 0; 
-   text-align: left;
-   font-weight: bold; 
-   font-size: x-large;
+  margin: 0.5em 0;
+  text-align: left;
+  font-weight: bold;
+  font-size: x-large;
 }
 
 div.head2dx {
-   margin: 0.5em 0; 
-   text-align: right;
-   font-weight: bold; 
-   font-size: x-large;
+  margin: 0.5em 0;
+  text-align: right;
+  font-weight: bold;
+  font-size: x-large;
 }
 
 div.head3sn {
-   margin: 0.5em 0; 
-   text-align: left;
-   font-weight: bold; 
-   font-size: large;
+  margin: 0.5em 0;
+  text-align: left;
+  font-weight: bold;
+  font-size: large;
 }
 
 div.text {
-   margin: 1em 0; 
-   text-align: left;
-   font-weight: normal; 
-   font-size: medium;
+  margin: 1em 0;
+  text-align: left;
+  font-weight: normal;
+  font-size: medium;
 }
 
 span.emph {
-   font-weight: bold;
-   font-size: medium;
+  font-weight: bold;
+  font-size: medium;
 }
 
 /* tables *******************************************************************/
@@ -85,28 +85,28 @@ td {
 /* inline decorations *******************************************************/
 
 img.icon32 {
-   border: 0; 
-   width: 32px; 
-   height: 32px;
+  border: 0;
+  width: 32px;
+  height: 32px;
 }
 
 img.icon37 {
-   border: 0; 
-   width: 37px; 
-   height: 37px;
+  border: 0;
+  width: 37px;
+  height: 37px;
 }
 
 img.rule {
-   border: 0; 
-   height: 4px;
-   width: 100%; 
+  border: 0;
+  height: 4px;
+  width: 100%;
 }
 
 img.w3c {
-   margin: 0 0.5em; 
-   border: 0; 
-   width: 88px; 
-   height: 32px; /* this should be 31px */
+  margin: 0 0.5em;
+  border: 0;
+  width: 88px;
+  height: 32px; /* this should be 31px */
 }
 
 /* foreground colors (life cycle, grammar) **********************************/
@@ -176,11 +176,11 @@ img.w3c {
 }
 
 .cyan {
-  background-color:#bfffff; /* + 3/4 */  
+  background-color:#bfffff; /* + 3/4 */
 }
 
 .water {
-  background-color:#ccffe5; /* + 4/5 */ 
+  background-color:#ccffe5; /* + 4/5 */
 }
 
 .green {
diff --git a/helm/www/lambdadelta/css/lddl.css b/helm/www/lambdadelta/css/lddl.css
index dbcb6c81f..48a2ba4d8 100644
--- a/helm/www/lambdadelta/css/lddl.css
+++ b/helm/www/lambdadelta/css/lddl.css
@@ -3,46 +3,51 @@
 /* terms ********************************************************************/
 
 .separator {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 0, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 0, 0);
 }
 
 .sort {
-   background: rgb(255, 255, 255); 
-   color: rgb(128, 0, 255);
+  background: rgb(255, 255, 255);
+  color: rgb(128, 0, 255);
 }
 
 .lref {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 0, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 0, 0);
 }
 
 .gref {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 0, 255);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 0, 255);
 }
 
 .appl {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 0, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 0, 0);
 }
 
 .cast {
-   background: rgb(255, 255, 255); 
-   color: rgb(255, 0, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(255, 0, 0);
 }
 
 .proj {
-   background: rgb(255, 255, 255); 
-   color: rgb(192, 120, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(192, 120, 0);
 }
 
 .local {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 160, 0);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 160, 0);
 }
 
 .global {
-   background: rgb(255, 255, 255); 
-   color: rgb(0, 0, 255);
+  background: rgb(255, 255, 255);
+  color: rgb(0, 0, 255);
+}
+
+.sup {
+  vertical-align: super;
+  font-size: smaller;
 }
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index 80ef0b0ab..13f9f92eb 100644
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -26,7 +26,7 @@
    
    <subsection name="v2"><img logo="ld2"/>λδ version 2 (active)</subsection>
    <body>
-      The main source of information is <notice class="alpha" notice="R2c"/>.
+      The main source of information is <notice class="alpha" notice="J2a"/>.
    </body>
    <table name="documentation_2"/>
 
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 76bd89b33..04ef6ed1a 100644
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -144,17 +144,17 @@
    <topitem name="contents">
       <notice class="alpha" notice="Contents:"/>
       Landau's "Grundlagen der Analysis"
-      (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
+      (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
    </topitem>
    <topitem name="access">
-      <notice class="alpha" notice="Access:"/>
-      <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
+      <notice class="alpha" notice="Access: "/>
+      <rlink to="html/lddl/">html pages</rlink> (updated <notice class="gamma" notice="2019-12"/>),
       <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
       <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
    </topitem>
    <topitem name="examples">
-      <notice class="alpha" notice="Examples:"/>
-      <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+      <notice class="alpha" notice="Examples: "/>
+      <rlink to="html/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
          Grundlagen's definition "t234"</rlink>
       in λδ version 4.
    </topitem>
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 82ce7d781..f5cdfbed0 100644
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -155,12 +155,17 @@
 </xsl:template>
 
 <xsl:template match="ld:style">
-   <span class="{@class}">
-      <xsl:choose>
-         <xsl:when test="@of"><xsl:value-of select="@of"/></xsl:when>
-         <xsl:otherwise><xsl:apply-templates/></xsl:otherwise>
-      </xsl:choose>
-   </span>
+  <span class="{@class}">
+    <xsl:choose>
+      <xsl:when test="@title">
+        <xsl:attribute name="title"><xsl:value-of select="@title"/></xsl:attribute>
+      </xsl:when>
+    </xsl:choose>
+    <xsl:choose>
+      <xsl:when test="@of"><xsl:value-of select="@of"/></xsl:when>
+      <xsl:otherwise><xsl:apply-templates/></xsl:otherwise>
+    </xsl:choose>
+  </span>
 </xsl:template>
 
 <xsl:template match="ld:notice">
diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl
index a126c9ba4..3685e8a71 100644
--- a/helm/www/lambdadelta/xslt/lddl_library.xsl
+++ b/helm/www/lambdadelta/xslt/lddl_library.xsl
@@ -13,7 +13,6 @@
 
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns="http://lambdadelta.info/"
-                              xmlns:xhtml="http://www.w3.org/1999/xhtml"
 >
 
 <xsl:template name="sp">
@@ -121,13 +120,13 @@
 </xsl:template>
 
 <xsl:template name="global">
-   <xhtml:span class="global" title="{@position}">
+   <style class="global" title="{@position}">
       <xsl:value-of select="@name"/>
-   </xhtml:span>
+   </style>
 </xsl:template>
 
 <xsl:template name="lddlurl">
-   <xsl:value-of select="'static/lddl'"/>
+   <xsl:value-of select="'html/lddl'"/>
 </xsl:template>
 
 <xsl:template name="mk_segment">
@@ -157,9 +156,9 @@
       </xsl:when>
       <xsl:otherwise>
          <xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
-         <xhtml:span class="global">
+         <style class="global">
 	    <xsl:value-of select="substring-after(@uri,$path)"/>
-         </xhtml:span>
+         </style>
       </xsl:otherwise>
    </xsl:choose>
 </xsl:template>
@@ -174,7 +173,7 @@
 </xsl:template>
 
 <xsl:template name="layer">
-   <xhtml:sup>
+   <style class="sup">
       <xsl:choose>
          <xsl:when test="@layer">
             <xsl:value-of select="@layer"/>
@@ -183,7 +182,7 @@
             <xsl:call-template name="infinity"/>
          </xsl:otherwise>
       </xsl:choose>
-   </xhtml:sup>
+   </style>
 </xsl:template>
 
 <xsl:template name="abst">
@@ -240,15 +239,15 @@
    <xsl:variable name="last">
       <xsl:value-of select="last()"/>
    </xsl:variable>
-   <xhtml:span class="separator" title="{$pos} {$last}">
+   <style class="separator" title="{$pos} {$last}">
       <xsl:call-template name="fs"/>
-   </xhtml:span>
+   </style>
 -->
    <xsl:choose>
       <xsl:when test="last()>position()">
-         <xhtml:span class="separator">
+         <style class="separator">
             <xsl:call-template name="fs"/>
-         </xhtml:span>
+         </style>
       </xsl:when>
    </xsl:choose>
 </xsl:template>
@@ -256,9 +255,9 @@
 <!--
 
 <xsl:template name="multiple">
-   <xhtml:span class="separator">
+   <style class="separator">
       <xsl:call-template name="cm"/>
-   </xhtml:span>
+   </style>
 </xsl:template>
 
 <xsl:template name="mk_terms">
diff --git a/helm/www/lambdadelta/xslt/lddl_term.xsl b/helm/www/lambdadelta/xslt/lddl_term.xsl
index dd5a45083..d09b113bc 100644
--- a/helm/www/lambdadelta/xslt/lddl_term.xsl
+++ b/helm/www/lambdadelta/xslt/lddl_term.xsl
@@ -13,86 +13,86 @@
 
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:ld="http://lambdadelta.info/"
-                              xmlns:xhtml="http://www.w3.org/1999/xhtml"
+                              xmlns="http://lambdadelta.info/"
 >
 
 <xsl:template match="ld:Sort">
-   <xhtml:span class="sort" title="{@position}">
+   <style class="sort" title="{@position}">
       <xsl:value-of select="@name"/>
-   </xhtml:span>
+   </style>
 </xsl:template>
 
 <xsl:template match="ld:LRef">
-   <xhtml:span class="lref" title="{@position}">
+   <style class="lref" title="{@position}">
       <xsl:value-of select="@name"/>
-   </xhtml:span>
+   </style>
 </xsl:template>
 
 <xsl:template match="ld:GRef">
-   <xhtml:span class="gref" title="{@position}&lt;{@uri}&gt;">
+   <style class="gref" title="{@position}&lt;{@uri}&gt;">
       <xsl:call-template name="uri"/>
-   </xhtml:span>
+   </style>
 </xsl:template>
 
 <xsl:template match="ld:Cast">
-   <xhtml:span class="cast">
+   <style class="cast">
       <xsl:call-template name="oa"/>
       <xsl:apply-templates select="*"/>
       <xsl:call-template name="ca"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
 <xsl:template match="ld:Appl">
-   <xhtml:span class="appl">
+   <style class="appl">
       <xsl:call-template name="op"/>
       <xsl:apply-templates select="*"/>
 <!--      <xsl:call-template name="mk_terms"/> -->
       <xsl:call-template name="cp"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
 <xsl:template match="ld:Proj">
-   <xhtml:span class="proj">
+   <style class="proj">
       <xsl:call-template name="oc"/>
       <xsl:apply-templates select="*"/>
       <xsl:call-template name="cc"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
 <xsl:template match="ld:Abst">
-   <xhtml:span class="local" title="{@position}">
+   <style class="local" title="{@position}">
       <xsl:call-template name="abst"/>
       <xsl:call-template name="ob"/>
       <xsl:call-template name="name"/>
       <xsl:call-template name="cn"/>
       <xsl:apply-templates select="*"/>
       <xsl:call-template name="cb"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
 <xsl:template match="ld:Abbr">
-   <xhtml:span class="local">
+   <style class="local">
       <xsl:call-template name="abbr"/>
       <xsl:call-template name="ob"/>
       <xsl:call-template name="name"/>
       <xsl:call-template name="eq"/>
       <xsl:apply-templates select="*"/>
       <xsl:call-template name="cb"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
 <xsl:template match="ld:Void">
-   <xhtml:span class="local">
+   <style class="local">
       <xsl:call-template name="void"/>
       <xsl:call-template name="ob"/>
       <xsl:call-template name="name"/>
       <xsl:call-template name="cb"/>
-   </xhtml:span>
+   </style>
    <xsl:call-template name="separator"/>
 </xsl:template>
 
-- 
2.39.2