From: Ferruccio Guidi Date: Sat, 14 Dec 2019 11:22:13 +0000 (+0100) Subject: web site update X-Git-Tag: make_still_working~210 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=9a0dc83131e9695ffd4254ff5546817ca431d8c2 web site update + updated generation procedure + updated generation software + updated css --- diff --git a/.gitignore b/.gitignore index 83073d3fc..224bc1923 100644 --- 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 df4a4b519..391b4e1f8 100644 --- 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 c22e290ac..9496cc7d2 100644 --- 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 " 🗏 %s.ld\n" oname base; + KP.fprintf och " \n" oname base; dirs | KU.S_DIR -> let oname = concats [st.bd; st.op; dname; name] in - KP.fprintf och " 🗁 %s/\n" oname name; + KP.fprintf och " \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 " \n"; + let dirs = Array.fold_left (out_entry st dname och) [] dir in + KP.fprintf och " \n"; + dirs let out_index st dname och = KP.fprintf och "\n\n"; diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index e60a6a46c..2f29e4bb7 100644 --- 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%s\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\n" (ind (i+3)); + P.fprintf och "%s\n" (ind (i+2)) xhtbl; A.iter (out_cell och) row; - P.fprintf och "%s\n" (ind (i+3)) + P.fprintf och "%s\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 "\n" name; - P.fprintf och "%s\n" (ind (i+1)); - P.fprintf och "%s\n" (ind (i+2)); - A.iter (out_row och) matrix.M.m; - P.fprintf och "%s\n" (ind (i+2)); + P.fprintf och "%s
\n" (ind (i+1)) xhtbl; + A.iter (out_row och) matrix.M.m; P.fprintf och "%s
\n" (ind (i+1)); P.fprintf och "\n\n" diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index 929330851..57e2774b2 100644 --- 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 48a2ba4d8..6db5f6843 100644 --- 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 5ef81f018..1a689f678 100644 --- 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 cd7c4121b..fffcc806a 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -35,8 +35,9 @@ to view this site correctly, please install fonts supporting Unicode 7.0 (June 2014). - For instance - or . + For instance + or + or . diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 3f840b7a0..e777c310a 100644 --- 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 d1faf246e..b81913727 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -130,6 +130,19 @@ + +
+ + + + + + + + + + +