web site update

+ updated generation procedure
+ updated generation software
+ updated css

diff --git a/.gitignore b/.gitignore
index 83073d3fcda2f7364a44c178ae4981b80eeb5574..224bc1923ba75a26ac8ba568345427a59e1e02a4 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -45,7 +45,8 @@ 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/etc/*.stamp
+helm/www/lambdadelta/etc/*.tar.bz2
 helm/www/lambdadelta/web/lddl
 helm/www/lambdadelta/xml/Environment
 helm/www/lambdadelta/xml/index.txt

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index df4a4b51942408d74a716fc85918d5464706eb97..391b4e1f883d524907b4b3b469df35ddda1a4736 100644 (file)
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -34,8 +34,12 @@ RXMLDIR  = $(RHOMEDIR)/xml
 RDOWNDIR = $(RHOMEDIR)/download
 RSTATICDIR = /projects/helm/public_html/lambda-delta/static
 
-DLHTMLSTAMP = $(ETCDIR)/lddl_html.stamp
-DLHTMLIXSTAMP = $(ETCDIR)/lddl_html_ix.stamp
+HTMLSTAMP   = $(ETCDIR)/html.stamp
+HTMLIXSTAMP = $(ETCDIR)/html_ix.stamp
+LDWSTAMP    = $(ETCDIR)/ldw.stamp
+LDWIXSTAMP  = $(ETCDIR)/ldw_ix.stamp
+
+SITEMAP     = $(XSLTDIR)/sitemap.xsl
 
 SLS     = helena.sl automath.sl
 BIB     = lambdadelta.bib
@@ -87,7 +91,7 @@ define HTML_TEMPLATE
        $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$<
 endef
 
-ifeq ($(MAKECMDGOALS), www)
+ifeq ($(MAKECMDGOALS), home)
    LDWS  = $(shell find -L $(WEBDIRS) -name "*.ldw.xml")
    TBLS  = $(shell find -L $(WEBDIRS) -name "*.tbl")
    XSLS  = $(addprefix $(XSLTDIR)/,xhtbl.xsl $(notdir $(TBLS:%.tbl=%.xsl)))
@@ -101,37 +105,35 @@ endif
 
 all:
 
-www: $(HTMLS) $(TBLS) $(XHTBL)
+# UPDATE HTML LDDL ###########################################################
 
-lint-xml: $(XMLS:%=$(XMLDIR)/%)
-       @echo XMLLINT --valid
-       $(H)$(XMLLINT) --valid $^
+$(ETCDIR)/html_lddl.tar.bz2: $(HTMLSTAMP)
+       @echo "  INSTALL html"
+       $(H)tar -cjf $@ $(HTMLDIR)
+       $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
+       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
 
-$(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
+up-html: $(ETCDIR)/html_lddl.tar.bz2
 
-$(DOWNDIR)/lddl.tar.bz2 lddl: $(ETCDIR)/exclude.txt $(XMLDIR)/index.txt
-       @echo "  GENERATE lddl.tar.bz2"
-       $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR)
+# UPDATE HTML IX LDDL ########################################################
 
-install-xml: $(DOWNDIR)/lddl.tar.bz2
-       @echo "  INSTALL xml"
-       $(H)scp $^ $(RDOWNDIR)
-       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2"
+$(ETCDIR)/html_lddl_ix.tar.bz2: $(HTMLIXSTAMP)
+       @echo "  INSTALL html-ix"
+       $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html`
+       $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
+       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
 
-test-html:
-       @$(MAKE) --no-print-directory $(XMLS:%.xml=%)
+up-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2
 
-html: $(ETCDIR)/make_html.sh
-       @echo "  MAKE */*.ld"
-#      $(H). $<
-       $(H)$(INDEX) -i $(LDDLDIR) -o $(HTMLDIR) .
+# UPDATE HTML HOME ###########################################################
+
+up-home:
+       @echo "  UPDATE $(RHOMEDIR)/html/"
+       $(H)scp -q html/*.html $(RHOMEDIR)/html/
 
-test: $(DLHTMLIXSTAMP)
+# GENERATE HTML LDDL #########################################################
 
-$(DLHTMLSTAMP):
+$(HTMLSTAMP): $(LDWSTAMP) $(SITEMAP)
        $(H)for LDW in `find $(LDDLDIR) -name *.ldw.xml`; do \
        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
@@ -139,9 +141,13 @@ $(DLHTMLSTAMP):
        $(XSLT) $(XSLT_OUT) $$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \
        done
        $(H)touch $@
-       $(H)touch $(DLHTMLIXSTAMP)
+       $(H)touch $(HTMLIXSTAMP)
+
+html: $(HTMLSTAMP)
+
+# GENERATE HTML IX LDDL ######################################################
 
-$(DLHTMLIXSTAMP):
+$(HTMLIXSTAMP): $(LDWIXSTAMP) $(SITEMAP)
        $(H)for LDW in `find $(LDDLDIR) -name index.ldw.xml`; do \
        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
@@ -150,21 +156,53 @@ $(DLHTMLIXSTAMP):
        done
        $(H)touch $@
 
-install-html: $(ETCDIR)/html_lddl.tar.bz2
+html-ix: $(HTMLIXSTAMP)
 
-$(ETCDIR)/html_lddl.tar.bz2:
-       @echo "  INSTALL html"
-       $(H)tar -cjf $@ $(HTMLDIR)
-       $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
-       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
+# GENERATE HTML HOME #########################################################
 
-install-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2
+home: $(HTMLS) $(TBLS) $(XHTBL)
 
-$(ETCDIR)/html_lddl_ix.tar.bz2:
-       @echo "  INSTALL html"
-#      $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html`
-       $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
-       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
+# GENERATE LDW LDDL ##########################################################
+
+$(LDWSTAMP):
+       $(H)touch $@
+
+ldw: $(LDWSTAMP)
+
+# GENERATE LDW IX LDDL #######################################################
+
+$(LDWIXSTAMP): $(INDEX)
+       $(H)$(INDEX) -i $(LDDLDIR) -o $(HTMLDIR) .
+       $(H)touch $@
+
+ldw-ix: $(LDWIXSTAMP)
+
+##############################################################################
+
+lint-xml: $(XMLS:%=$(XMLDIR)/%)
+       @echo XMLLINT --valid
+       $(H)$(XMLLINT) --valid $^
+
+$(ETCDIR)/make_html.sh $(XMLDIR)/index.txt index:
+       @echo "  GENERATE INDEXES"
+       $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt
+       $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh
+
+$(DOWNDIR)/lddl.tar.bz2 lddl: $(ETCDIR)/exclude.txt $(XMLDIR)/index.txt
+       @echo "  GENERATE lddl.tar.bz2"
+       $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR)
+
+install-xml: $(DOWNDIR)/lddl.tar.bz2
+       @echo "  INSTALL xml"
+       $(H)scp $^ $(RDOWNDIR)
+       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2"
+
+test-html:
+       @$(MAKE) --no-print-directory $(XMLS:%.xml=%)
+
+# html: $(ETCDIR)/make_html.sh
+#      @echo "  MAKE */*.ld"
+#      $(H). $<
 
 install-jed: $(SLS:%=$(JEDDIR)/%)
        @echo "  INSTALL $(SLS)"
@@ -199,10 +237,6 @@ install-v: $(HELENADIR)/$(COQ)
        @echo "  INSTALL $(notdir $<)"
        $(H)scp $< $(DOWNDIR)
 
-up-html:
-       @echo "  UPDATE $(RHOMEDIR)/html/"
-       $(H)scp -q html/*.html $(RHOMEDIR)/html/
-
 up-css:
        @echo "  UPDATE $(RHOMEDIR)/css/"
        $(H)scp -q -r css $(RHOMEDIR)
@@ -215,8 +249,8 @@ up-download:
        @echo "  UPDATE $(RHOMEDIR)/download/"
        $(H)scp -q -r download $(RHOMEDIR)
 
-%.ld:
-       @echo "  XSLT $@"
+#%.ld:
+#      @echo "  XSLT $@"
 #      $(H)mkdir -p $(LDDLDIR)/$(@D)
 #      $(H)$(XSLT) --novalid $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
 #      $(H)mkdir -p $(HTMLDIR)/$(@D)

diff --git a/helm/www/lambdadelta/bin/index/index.ml b/helm/www/lambdadelta/bin/index/index.ml
index c22e290acd73f9befa4322f511ea591ec16866db..9496cc7d2e806635ba83826f8f06492c96254dac 100644 (file)
--- a/helm/www/lambdadelta/bin/index/index.ml
+++ b/helm/www/lambdadelta/bin/index/index.ml
@@ -43,11 +43,11 @@ let out_entry st dname och dirs name =
   | KU.S_REG when KF.check_suffix name i_ext ->
     let base = KF.chop_suffix name i_ext in 
     let oname = concats [st.bd; st.op; dname; base^o_ext] in
-    KP.fprintf och "    <line class=\"global emph\">&#x1F5CF; <rlink to=\"%s\">%s.ld</rlink></line>\n" oname base;
+    KP.fprintf och "    <file class=\"global emph\" type=\"&#x1F5CF;\" to=\"%s\" name=\"%s.ld\"/>\n" oname base;
     dirs
   | KU.S_DIR ->
     let oname = concats [st.bd; st.op; dname; name] in
-    KP.fprintf och "    <line class=\"alpha emph\">&#x1F5C1; <rlink to=\"%s\">%s/</rlink></line>\n" oname name;
+    KP.fprintf och "    <file class=\"alpha emph\" type=\"&#x1F5C1;\" to=\"%s\" name=\"%s/\"/>\n" oname name;
     name :: dirs
   | _        ->
     dirs
@@ -60,7 +60,10 @@ let list_dir st dname och =
   let iname = concats [st.bd; st.ip; dname] in
   let dir = Sys.readdir iname in
   Array.sort String.compare dir;
-  Array.fold_left (out_entry st dname och) [] dir
+  KP.fprintf och "   <index>\n";
+  let dirs = Array.fold_left (out_entry st dname och) [] dir in
+  KP.fprintf och "   </index>\n";
+  dirs
 
 let out_index st dname och =
   KP.fprintf och "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n\n";

diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
index e60a6a46c3e21a792577c35216046de44d41d2d5..2f29e4bb728192f22c7f5142428826d63013597e 100644 (file)
--- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
@@ -8,6 +8,8 @@ module O = Options
 module T = Table
 module M = Matrix
 
+let xhtbl = "xhtbl"
+
 let i = 0
 
 let myself = F.basename (Sys.argv.(0))
@@ -46,14 +48,14 @@ let key cell =
 let ind i = S.make (2 * i) ' '
 
 let out_cell och cell =
-   let cc = border cell in
+   let cc = xhtbl :: border cell in
    P.fprintf och "%s<td class=\"%s\"%s>%s</td>\n"
-      (ind (i+4)) (S.concat " " cc) (name cell) (key cell)
+      (ind (i+3)) (S.concat " " cc) (name cell) (key cell)
 
 let out_row och row =
-   P.fprintf och "%s<tr>\n" (ind (i+3));
+   P.fprintf och "%s<tr class=\"%s\">\n" (ind (i+2)) xhtbl;
    A.iter (out_cell och) row;
-   P.fprintf och "%s</tr>\n" (ind (i+3))
+   P.fprintf och "%s</tr>\n" (ind (i+2))
 
 let out_space och (name, uri) =
    let name = if name = "" then name else ":" ^ name in
@@ -74,10 +76,8 @@ let open_out name spaces =
 
 let output och name matrix =
    P.fprintf och "<xsl:template name=\"%s\">\n" name;
-   P.fprintf och "%s<table cellpadding=\"4\" cellspacing=\"0\">\n" (ind (i+1));
-   P.fprintf och "%s<tbody>\n" (ind (i+2));
-   A.iter (out_row och) matrix.M.m; 
-   P.fprintf och "%s</tbody>\n" (ind (i+2));
+   P.fprintf och "%s<table class=\"%s\" cellpadding=\"4\" cellspacing=\"0\">\n" (ind (i+1)) xhtbl;
+   A.iter (out_row och) matrix.M.m;
    P.fprintf och "%s</table>\n" (ind (i+1));
    P.fprintf och "</xsl:template>\n\n"
 

diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css
index 929330851d8c4cd1ad5aeb09a56fd4c83feb648e..57e2774b2ad1131a310b07d082f4a4eac07bbff7 100644 (file)
--- a/helm/www/lambdadelta/css/ld_web.css
+++ b/helm/www/lambdadelta/css/ld_web.css
@@ -63,25 +63,6 @@ div.text {
   font-size: medium;
 }
 
-span.emph {
-  font-weight: bold;
-  font-size: medium;
-}
-
-/* tables *******************************************************************/
-
-table {
-  margin-left: auto;
-  margin-right: auto;
-  width: 100%;
-}
-
-td {
-  border-color:#000000;
-  border-width:1px;
-  color:#000000;
-}
-
 /* inline decorations *******************************************************/
 
 img.icon32 {

diff --git a/helm/www/lambdadelta/css/lddl.css b/helm/www/lambdadelta/css/lddl.css
index 48a2ba4d8cb89843ddc21c4e4c984a95b73eaa8e..6db5f68431d2b2604d53a8d292c393400b97012e 100644 (file)
--- a/helm/www/lambdadelta/css/lddl.css
+++ b/helm/www/lambdadelta/css/lddl.css
@@ -1,5 +1,12 @@
 @charset "UTF-8";
 
+/* objects ******************************************************************/
+
+.emph {
+  font-weight: bold;
+  font-size: medium;
+}
+
 /* terms ********************************************************************/
 
 .separator {

diff --git a/helm/www/lambdadelta/css/xhtbl.css b/helm/www/lambdadelta/css/xhtbl.css
index 5ef81f018e68a45edcaab910f2986eafa290ded7..1a689f678c47aa89cef804e96c286e73f06fb4ea 100644 (file)
--- a/helm/www/lambdadelta/css/xhtbl.css
+++ b/helm/www/lambdadelta/css/xhtbl.css
@@ -1,5 +1,19 @@
 @charset "UTF-8";
 
+/* tables *******************************************************************/
+
+table.xhtbl {
+  margin-left: auto;
+  margin-right: auto;
+  width: 100%;
+}
+
+td.xhtbl {
+  border-color:#000000;
+  border-width:1px;
+  color:#000000;
+}
+
 /* cell borders *************************************************************/
 
 td.nnnn {

diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index cd7c4121b33746a37dda80f6661fa1922a32e59e..fffcc806a802007222037e14953546ad5bd93592 100644 (file)
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -35,8 +35,9 @@
       <notice class="alpha" text="Notice:"/>
       to view this site correctly, please install fonts
       supporting <link to="http://www.unicode.org/">Unicode 7.0</link> (June 2014).
-      For instance <notice class="alpha" text="Unifont"/>
-      or <notice class="alpha" text="Symbola"/>.
+      For instance <notice class="alpha" text="Unifont Upper"/>
+      or <notice class="alpha" text="Symbola"/>
+      or <notice class="alpha" text="Noto Sans Symbols2"/>.
    </body>
    <body>
       <ucs-bronze char="03BB"/>

diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 3f840b7a09e97730ec7a7f3515aae01465968ccd..e777c310aaa7f34c5e0438a755a3d6267433d003 100644 (file)
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -38,7 +38,7 @@ table [
         @@("osn/" "Open Symbolic Notation (OSN)") 
       * ]
       [ @@("html/implementation#lddl" "library")
-        "(" ^ @@("static/lddl/" "static LDDL directory") ^ ")"
+        "(" ^ @@("html/lddl/" "static LDDL directory") ^ ")"
       * ]
    }
 ]

diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index d1faf246e920198a5c470110b7edf6168b39d67e..b819137274cd6b05b4ccf95396fec4d2ab7deecd 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -130,6 +130,19 @@
    </div>
 </xsl:template>
 
+<xsl:template match="ld:index">
+   <table><xsl:apply-templates/></table>
+</xsl:template>
+
+<xsl:template match="ld:file">
+   <tr class="{@class}">
+     <td class="center"><xsl:value-of select="@type"/></td>
+     <td><a href="{$baseurl}{@to}">
+       <xsl:value-of select="@name"/>
+     </a></td> 
+   </tr>
+</xsl:template>
+
 <xsl:template match="ld:link">
    <a href="{@to}">
       <xsl:apply-templates/>