From: Ferruccio Guidi Date: Thu, 7 Apr 2016 13:34:39 +0000 (+0000) Subject: - advances in the site generation architecture X-Git-Tag: make_still_working~611 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f39d53ed5f2a11cacbfabf5348e01b47d19479e5;p=helm.git - advances in the site generation architecture - more on OSN and on the disclaimer --- diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index a735efdac..9f2e42d59 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -131,6 +131,20 @@ img.w3c { color:#000080; } +/* mark colors **************************************************************/ + +.red-mark { + color:#F00000; +} + +.green-mark { + color:#00F000; +} + +.blue-mark { + color:#0000F0; +} + /* background colors ********************************************************/ .white { diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index db2189cc6..6ce59cb79 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -3,6 +3,7 @@ @@ -17,19 +18,19 @@ (revised ). - λδ version 3 (proposed) + λδ version 3 (proposed) The main source of information is . - λδ version 2 (active) + λδ version 2 (active) The main source of information is .
- λδ version 1 (superseded) + λδ version 1 (superseded) The main source of information is . A summary is available in . diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 229c5e88b..32139b3a6 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,36 +3,25 @@ Tools - λδ Digital Library (LDDL) + Open Symbolic Notation + - The λδ Digital Library is part of HELM - and contains resources expressed in the systems of the λδ family. + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal systems. + Additional information will appear soon. - - - Landau's "Grundlagen der Analysis" - (from Jutting's specification in Automath). - - - - static pages (updated ), - data set (updated ), - HELM server URL (updated ). - - - - - Grundlagen's definition "t234" - in λδ version 4. - - Helena + + Helena Helena is a processor for the systems of the λδ family, @@ -146,72 +135,29 @@ - Open Symbolic Notation - - Open Symbolic Notation (OSN) is an easy data-interchange textual format - based on symbolic expressions. - OSN is completely language independent but uses widely accepted conventions. - These features make OSN ideal for storing and exchanging tree-like data structures - in a lightweight manner. - + λδ Digital Library (LDDL) + - An OSN text uses the UTF-8 character set - and contains the next tokens: + The λδ Digital Library is part of HELM + and contains resources expressed in the systems of the λδ family. - - - - - - - - - - - - - this token can represent the identifiers and the numerical constants of most programming languages; - - - - - - - - - - every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ - the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ - morover, the escape sequences \x <two hexadecimal digits> and \u <four hexadecimal digits> - allow to specify a character by its code point - finally the escape sequences \( for U+0002 and \) for U+0003 are available - - - - - - - - - - - this token starts a compound symbolic expression; - - - - - - - this token ends a compound symbolic expression; - - <ignored> each of the characters U+0009..U+000D U+0020 , ; = - these characters are ignored and separate the other tokens - - <reserved> any character not starting any other token - these characters are not allowed, - and those in the range U+0021..U+007E are - ! # $ % & ' * / ? @ \ ^ ` | ~ - + + + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). + + + + static pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + + + Grundlagen's definition "t234" + in λδ version 4. +
diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index 9913b2401..13eab16ba 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -3,6 +3,7 @@ @@ -85,8 +86,8 @@ Disclaimer - The systens of the λδ family related intentionally to any other system - having (variations of) the symbols λ and δ in its name or syntax. + The systens of the λδ family related intentionally to + any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to): @@ -143,5 +144,12 @@ Eindhoven University of Technology, Eindhoven. + + Moreover, the systens of the λδ family related intentionally to + the character Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. + +
diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 2e6e14936..0bf225624 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -3,6 +3,7 @@ diff --git a/helm/www/lambdadelta/web/home/osn.ldw.xml b/helm/www/lambdadelta/web/home/osn.ldw.xml new file mode 100644 index 000000000..ef8580bb8 --- /dev/null +++ b/helm/www/lambdadelta/web/home/osn.ldw.xml @@ -0,0 +1,178 @@ + + + + + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal systems. + In order to meet theese design goals, OSN pursues the following features. + + + + + + + + + + + + + Syntax + + + An OSN text uses the UTF-8 character set + and contains the next seven tokens that we define in a very common EBNF variant. + Characters not starting a token are not allowed. + The ones in the range U+0021 ... U+007E are ! # $ % & * / ? @ \ ^ | ~ + and are available for extensions of OSN. + + + + + + + + + + + + + + + this token can represent the identifiers and the numerical constants of most programming languages; + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + this token contains free-form text with commonly accepted escape sequences; + + + + + + + + + + + + + this token is a widely used alternative of the former; + + + + + this token separates the qualifiers of a symbolic expression; + + + + + + + this token starts a compound symbolic expression; + + + + + + + this token ends a compound symbolic expression; + + + + + + + + this token is ignored and separates the other tokens. + + + + + + + +
+ diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index af3b9f773..8862f01d4 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -31,10 +31,10 @@ table [ } class "green" { [ @@"implementation" * ] + [ @@("implementation#helena" "helena") * ] [ @@("implementation#lddl" "library") "(" ^ @@("static/lddl/" "static LDDL directory") ^ ")" * ] - [ @@("implementation#helena" "helena") * ] } ] diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 969e3fd00..e3f4baf3b 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -3,6 +3,7 @@ @@ -46,7 +47,7 @@ - λδ version 3 (proposed) + λδ version 3 (proposed) The formal specification of λδ version 3 is forthcoming. @@ -54,7 +55,7 @@ - λδ version 2 (active) + λδ version 2 (active) The formal specification of λδ version 2 is available in the following formats: @@ -87,7 +88,7 @@ - λδ version 1 (superseded) + λδ version 1 (superseded) The formal specification of λδ version 1 is available in the following formats: diff --git a/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl b/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl index 5599defa6..5378a111e 100644 --- a/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl @@ -13,9 +13,7 @@ - < - > @@ -24,28 +22,48 @@ - + " " - + ' ' + + # + + + + + + , + + + | + | + ... + | + + + + + - + @@ -63,8 +81,26 @@ + + * + + 1 + + + - + + 1 + + * + + + + + + + * + + diff --git a/helm/www/lambdadelta/xslt/ld_web_library.xsl b/helm/www/lambdadelta/xslt/ld_web_library.xsl index fb76831dc..ad10ba2eb 100644 --- a/helm/www/lambdadelta/xslt/ld_web_library.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_library.xsl @@ -5,18 +5,6 @@ xmlns="http://www.w3.org/1999/xhtml" > - -
- - [\lambda\delta home] - -
-
-
- + + + [Valid XHTML 1.1] - + [Valid CSS level 2] - + [Generated from XML via XSL] - + [PNG used here] - + [Viewable with any browser] - + [Powered by Helena \lambda\delta processor] + + + + [\lambda\delta home] + + + + + + + + + + + + + + + + + + + + + + [Open Symbolic Notation logo] + + + + [Helena logo] + + + + [\lambda\delta digital library logo] + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index e3d04bbaf..4be8878ff 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -144,6 +144,15 @@
  • + + + + + + + + + @@ -162,64 +171,25 @@ - - - - - - - - - - - - - - - - - - - - - - - [Crux logo] - - - - - [Helena logo] - - - - - [Open Symbolic Notation logo] - + + + + + + +

    - - - + + + - - + +

    @@ -228,10 +198,6 @@
    - - - - @@ -253,7 +219,7 @@ href="{$baseurl}images/crux_16.ico" /> - +