From 552427acaacc2ebd0737c2b6038085f7ea5f423b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Sep 2009 20:47:06 +0000 Subject: [PATCH] xml: first ld to xml stylesheets Makefile: we now generate index.txt dual_rg: automath encoding fixed --- helm/software/lambda-delta/.depend.opt | 10 +++ helm/software/lambda-delta/Makefile | 13 ++++ helm/software/lambda-delta/Makefile.common | 3 + helm/software/lambda-delta/dual_rg/drg.ml | 3 +- helm/software/lambda-delta/dual_rg/drgAut.ml | 6 +- .../lambda-delta/xml/ld-html-entry.xsl | 31 ++++++++ .../lambda-delta/xml/ld-html-library.xsl | 77 +++++++++++++++++++ .../lambda-delta/xml/ld-html-root.xsl | 55 +++++++++++++ .../lambda-delta/xml/ld-html-term.xsl | 57 ++++++++++++++ helm/software/lambda-delta/xml/ld-html.xsl | 20 +++++ 10 files changed, 270 insertions(+), 5 deletions(-) create mode 100644 helm/software/lambda-delta/xml/ld-html-entry.xsl create mode 100644 helm/software/lambda-delta/xml/ld-html-library.xsl create mode 100644 helm/software/lambda-delta/xml/ld-html-root.xsl create mode 100644 helm/software/lambda-delta/xml/ld-html-term.xsl create mode 100644 helm/software/lambda-delta/xml/ld-html.xsl diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index e235d685e..fe670cb6c 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,9 +1,17 @@ +lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi +lib/cps.cmo: +lib/cps.cmx: +lib/share.cmo: +lib/share.cmx: +lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +automath/aut.cmo: +automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -17,8 +25,10 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx +common/hierarchy.cmi: common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi +common/output.cmi: common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi common/entity.cmo: lib/nUri.cmi automath/aut.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 665972224..96412768c 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -35,3 +35,16 @@ hal: $(MAIN).opt xml-si: $(MAIN).opt @echo " HELENA -u -x $(INPUT)" $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > log.txt + +html: + @$(MAKE) --no-print-directory grundlagen/l/not.ld + +%.ld: BASEURL = --stringparam baseurl $(STATIC) + +%.ld: + @echo " XSLT $@" + $(H)mkdir -p static/$(@D) + $(H)$(XSLT) -o static/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml + +index: + find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 1af0e3abb..0cf1f84ac 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -1,5 +1,7 @@ H=@ +STATIC = http://helm.cs.unibo.it/lambda-delta/static + DIRECTORIES = $(shell cat Make) INCLUDES = $(DIRECTORIES:%=-I %) @@ -9,6 +11,7 @@ OCAMLOPT = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES) OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v XMLLINT = xmllint --noout +XSLT = xsltproc TAR = tar -czf $(MAIN:%=%.tgz) define DIR_TEMPLATE diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index 1d94a2643..e598a5986 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -28,9 +28,8 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | LRef of attrs * int (* attrs, position index *) | GRef of attrs * uri (* attrs, reference *) | Cast of attrs * term * term (* attrs, domain, element *) - | Proj of attrs * lenv * term (* attrs, closure, scope *) | Appl of attrs * term list * term (* attrs, arguments, function *) - | Bind of bind * term (* binder, scope *) + | Bind of lenv * term (* closure, scope *) and lenv = bind list (* local environment *) diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index c978c4a63..3b371afd7 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -108,7 +108,7 @@ let rec xlate_term f st lenv = function | A.Abst (name, w, t) -> let f ww = let b = mk_abst name ww in - let f tt = f (D.Bind (b, tt)) in + let f tt = f (D.Bind ([b], tt)) in xlate_term f st (b :: lenv) t in xlate_term f st lenv w @@ -160,7 +160,7 @@ let xlate_entity f st = function let f cnt = let f qid = let f ww = - let b = D.Abst ([], D.Proj ([], cnt, ww)) in + let b = D.Abst ([], D.Bind (cnt, ww)) in let entry = st.line, uri_of_qid qid, b in H.add st.henv (uri_of_qid qid) cnt; f {st with line = succ st.line} (Some entry) @@ -175,7 +175,7 @@ let xlate_entity f st = function let f qid = let f ww vv = let a = if trans then [] else [D.Priv] in - let b = D.Abbr (a, D.Proj ([], cnt, D.Cast ([], ww, vv))) in + let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in let entry = st.line, uri_of_qid qid, b in H.add st.henv (uri_of_qid qid) cnt; f {st with line = succ st.line} (Some entry) diff --git a/helm/software/lambda-delta/xml/ld-html-entry.xsl b/helm/software/lambda-delta/xml/ld-html-entry.xsl new file mode 100644 index 000000000..d6dbedd45 --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html-entry.xsl @@ -0,0 +1,31 @@ + + + + + + + +

+ Declaration: + +

+
+ + + +

+ Definition: + +

+
+ + + +

+ Exclusion: + +

+
+ + + diff --git a/helm/software/lambda-delta/xml/ld-html-library.xsl b/helm/software/lambda-delta/xml/ld-html-library.xsl new file mode 100644 index 000000000..9e09b447b --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html-library.xsl @@ -0,0 +1,77 @@ + + + + + + + + + + . + + + + ( + + + + ) + + + + < + + + + > + + + + : + + + + = + + + + &lambda; + + + + &delta; + + + + &chi; + + + + + + + + + + + + + .html + + + + + + + + + + + + + + + + + + diff --git a/helm/software/lambda-delta/xml/ld-html-root.xsl b/helm/software/lambda-delta/xml/ld-html-root.xsl new file mode 100644 index 000000000..a0b490753 --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html-root.xsl @@ -0,0 +1,55 @@ + + + + + + + + + + lambda-delta digital library (LDDL) + + +

+ + [lambda-delta-home] +

+

+
+ + [Valid HTML 4.01 Transitional] + + [Use any browser here] + [png used here] +
+ + + + +

+
+ Validation parameters: + sort hierarchy = "", + kernel options = "" +
+ + + diff --git a/helm/software/lambda-delta/xml/ld-html-term.xsl b/helm/software/lambda-delta/xml/ld-html-term.xsl new file mode 100644 index 000000000..a83c08088 --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html-term.xsl @@ -0,0 +1,57 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/software/lambda-delta/xml/ld-html.xsl b/helm/software/lambda-delta/xml/ld-html.xsl new file mode 100644 index 000000000..b66dd6f52 --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html.xsl @@ -0,0 +1,20 @@ + + + + + + + + + + + + + + -- 2.39.2