From: Ferruccio Guidi Date: Wed, 11 Dec 2019 22:40:24 +0000 (+0100) Subject: web site update X-Git-Tag: make_still_working~211 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7bb7028a9aafcfd5c6570f4ad5ca472f19691bfc web site update + updated automation for the generated LDDL web site + minor improvements --- diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 51ecbd1a5..df4a4b519 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -1,3 +1,4 @@ +SHELL := $(shell which bash) H=@ TAGS = www up-html up-css up-images up-download \ @@ -17,6 +18,7 @@ XMLDIR = xml SRCDIR = web/home LDDLDIR = web/lddl XHTBLDIR = bin/xhtbl +INDEXDIR = bin/index HTMLDIR = html/lddl JEDDIR = $(HOME)/mps/jed BIBDIR = $(HOME)/texmf/bibtex/bib @@ -32,6 +34,9 @@ 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 + SLS = helena.sl automath.sl BIB = lambdadelta.bib CONTRIB = lambdadelta_2.tar.gz @@ -52,6 +57,7 @@ MATITA = matita/root matita/grundlagen_2.ma XMLLINT = xmllint --noout XSLT = xsltproc XHTBL = $(XHTBLDIR)/xhtbl.native +INDEX = $(INDEXDIR)/index.native XHTBLOPTS = @@ -94,7 +100,6 @@ ifeq ($(MAKECMDGOALS), www) endif all: - @echo $(HTMLS) www: $(HTMLS) $(TBLS) $(XHTBL) @@ -121,13 +126,45 @@ test-html: html: $(ETCDIR)/make_html.sh @echo " MAKE */*.ld" - $(H). $< +# $(H). $< + $(H)$(INDEX) -i $(LDDLDIR) -o $(HTMLDIR) . + +test: $(DLHTMLIXSTAMP) + +$(DLHTMLSTAMP): + $(H)for LDW in `find $(LDDLDIR) -name *.ldw.xml`; do \ + TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ + echo " XSLT $$LDW"; \ + mkdir -p $${HTML%/*}; \ + $(XSLT) $(XSLT_OUT) $$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \ + done + $(H)touch $@ + $(H)touch $(DLHTMLIXSTAMP) + +$(DLHTMLIXSTAMP): + $(H)for LDW in `find $(LDDLDIR) -name index.ldw.xml`; do \ + TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ + echo " XSLT $$LDW"; \ + mkdir -p $${HTML%/*}; \ + $(XSLT) $(XSLT_OUT) $$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \ + done + $(H)touch $@ + +install-html: $(ETCDIR)/html_lddl.tar.bz2 + +$(ETCDIR)/html_lddl.tar.bz2: + @echo " INSTALL html" + $(H)tar -cjf $@ $(HTMLDIR) + $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) + $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" + +install-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2 -install-html $(DOWNDIR)/static_lddl.tar.bz2: $(ETCDIR)/exclude.txt $(ETCDIR)/make_html.sh +$(ETCDIR)/html_lddl_ix.tar.bz2: @echo " INSTALL html" - $(H)tar -cjf $(DOWNDIR)/static_lddl.tar.bz2 -C static -X $< lddl - $(H)scp $(DOWNDIR)/static_lddl.tar.bz2 $(RDOWNDIR) - $(H)ssh $(REMOTE) "cd $(RSTATICDIR) && tar -xjf ../../lambdadelta/download/static_lddl.tar.bz2 +# $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html` + $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) + $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" install-jed: $(SLS:%=$(JEDDIR)/%) @echo " INSTALL $(SLS)" @@ -180,9 +217,9 @@ up-download: %.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) - $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml +# $(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) +# $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml .PHONY: $(TAGS) diff --git a/helm/www/lambdadelta/bin/index/index.ml b/helm/www/lambdadelta/bin/index/index.ml index c7fd48d90..c22e290ac 100644 --- a/helm/www/lambdadelta/bin/index/index.ml +++ b/helm/www/lambdadelta/bin/index/index.ml @@ -2,48 +2,119 @@ module KF = Filename module KP = Printf module KU = Unix -let out_entry dname och dirs name = - let fname = KF.concat dname name in - let stats = KU.lstat fname in +type status = { +(* base directory *) + bd: string; +(* input prefix *) + ip: string; +(* output prefix *) + op: string; +(* current path *) + cp: string list +} + +let initial_status = { + bd = ""; ip = ""; op = ""; + cp = []; +} + +let imp_st = ref initial_status + +let i_ext = ".ld.ldw.xml" +let o_ext = ".ld.html" + +let concats l = + List.fold_left KF.concat "" l + +let concat st dname = {st with + ip = KF.concat st.ip dname; op = KF.concat st.op dname; +} + +let normalize dname = + if dname = KF.current_dir_name then "" else dname + +let mk_rlink s_to s_body = + KP.sprintf "%s" s_to s_body + +let out_entry st dname och dirs name = + let iname = concats [st.bd; st.ip; dname; name] in + let stats = KU.lstat iname in match stats.KU.st_kind with - | KU.S_REG -> - KP.fprintf och " %s\n" fname 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 " 🗏 %s.ld\n" oname base; dirs - | KU.S_DIR -> name :: dirs - | _ -> dirs + | KU.S_DIR -> + let oname = concats [st.bd; st.op; dname; name] in + KP.fprintf och " 🗁 %s/\n" oname name; + name :: dirs + | _ -> + dirs + +let mk_path st och = + let path = String.concat "/" (List.rev st.cp) in + KP.fprintf och " Contents of %s/\n" path -let list_dir dname och = - let dir = Sys.readdir dname in +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 dname och) [] dir + Array.fold_left (out_entry st dname och) [] dir -let out_index dname och = +let out_index st dname och = KP.fprintf och "\n\n"; - KP.fprintf och "\n"; KP.fprintf och " \n"; KP.fprintf och " Index\n"; - KP.fprintf och " \n"; - + KP.fprintf och " \n"; + mk_path st och; KP.fprintf och " \n"; KP.fprintf och " \n"; - let dirs = list_dir dname och in + let dirs = list_dir st dname och in KP.fprintf och " \n"; - KP.fprintf och "
\n"; + KP.fprintf och "
\n"; KP.fprintf och "\n"; dirs -let rec out_dir dname = - let och = open_out (KF.concat dname "index.ldw.xml") in - let dirs = out_index dname och in +let rec out_dir st dname = + let s_to, s_body = + if dname = "" + then concats [st.bd; st.op], "ld:" + else concats [st.bd; st.op; dname], dname + in + let st = {st with cp = mk_rlink s_to s_body :: st.cp} in + let oname = concats [st.bd; st.ip; dname; "index.ldw.xml"] in + let och = open_out oname in + let dirs = out_index st dname och in close_out och; - let map name = out_dir (KF.concat dname name) in - List.iter map dirs + let map st = out_dir (concat st dname) in + List.iter (map st) dirs + +let help_b = " Set this base directory" +let help_i = " Set this input prefix" +let help_o = " Set this output prefix" +let help = "Usage: index [ -bio | ]*" + +let set_b bd = + imp_st := {!imp_st with bd = normalize bd} + +let set_i ip = + imp_st := {!imp_st with ip = normalize ip} + +let set_o op = + imp_st := {!imp_st with op = normalize op} -let help = "Usage: index [ ]*" +let process dname = + out_dir !imp_st (normalize dname) let main = Arg.parse [ - ] out_dir help + "-b", Arg.String set_b, help_b; + "-i", Arg.String set_i, help_i; + "-o", Arg.String set_o, help_o; + ] process help diff --git a/helm/www/lambdadelta/images/bronze-03B4.png b/helm/www/lambdadelta/images/bronze-03B4.png new file mode 100644 index 000000000..d65392f09 Binary files /dev/null and b/helm/www/lambdadelta/images/bronze-03B4.png differ diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index 5625cdb8c..cd7c4121b 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -22,7 +22,7 @@ as a set of machine-checked digital specifications. - + λδ-2B for for Matita 0.99.4 (released: ). Documentation (J2a). @@ -33,11 +33,14 @@ - to view this site correctly, please select a font - with Unicode support. + to view this site correctly, please install fonts + supporting Unicode 7.0 (June 2014). + For instance + or . + diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index f5cdfbed0..d1faf246e 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -154,6 +154,15 @@
    • + +
    + + + + +
    +     + diff --git a/helm/www/lambdadelta/xslt/lddl_root.xsl b/helm/www/lambdadelta/xslt/lddl_root.xsl index 5645dc7e8..43aa1656e 100644 --- a/helm/www/lambdadelta/xslt/lddl_root.xsl +++ b/helm/www/lambdadelta/xslt/lddl_root.xsl @@ -23,7 +23,7 @@ > -
    +