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 ).
The main source of information is .
The main source of information is .
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"
>
-
-