X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fosn.html;h=e1cd36152f15a4159de2c65384228683a74a61cd;hb=aeb003ab531d9b9faffd46c47204b564009063cf;hp=db920807379c51a17cb8b2444329ddfe967670c8;hpb=7c3dc0455368fe74858226ab6cf3c19f68d0e2a7;p=helm.git
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html
index db9208073..e1cd36152 100644
--- a/helm/www/lambdadelta/osn.html
+++ b/helm/www/lambdadelta/osn.html
@@ -49,7 +49,8 @@
which targets the data structures of formal languages.
-
+
+
-
Optionally qualified symbolic expressions
@@ -60,7 +61,8 @@
data from different domains is added to the text they process.
-
+
+
-
The US-ASCII character set,
@@ -86,37 +88,43 @@
symbol = 1 * symbol-char ;
symbol-char = '+' | '-' | '.' | '0' | ... | '9' | 'A' | ... | 'Z' | '_' | '`' | 'a' | ... | 'z' ;
-
+
+
-
This token contains free-form text with commonly accepted escape sequences:
string = '"' , * ( string-char | "'" | '\' escape ) , '"' ;
string-char = ( #0 | ... | #10FFFF ) - ( #0 | ... | #1F | "'" | '\' | '"' | #7F ) ;
escape = 1 * space | '"' | "'" | '(' | ')' | '0' | '\' | 'a' | 'b' | 'e' | 'f' | 'n' | 'r' | 't' | ( 'u' , 4 * 4 hex ) | 'v' | ( 'x' , 2 * 2 hex ) ;
space = #9 | ... | #D | #20 ;
hex = '0' | ... | '9' | 'A' | ... | 'F' | 'a' | ... | 'f' ;
-
+
+
-
This token is a widely used alternative of the former token:
string-alt = "'" , * ( string-char | '"' | '\' escape ) , "'" ;
-
+
+
-
This token separates the qualifiers of a symbolic expression:
sep = ':' ;
-
+
+
-
This token starts a compound symbolic expression:
open = '(' | '<' | '[' | '{' ;
-
+
+
-
This token ends a compound symbolic expression:
close = ')' | '>' | ']' | '}' ;
-
+
+
-
This token is ignored and separates the other tokens:
@@ -133,13 +141,15 @@
text = * q-expr ;
-
+
+
-
A qualified symbolic expression:
q-expr = * ( symbol , 1 * sep ) , expr ;
-
+
+
-
An unqualified symbolic expression:
@@ -187,6 +197,6 @@
- Last update: Fri, 22 Jul 2016 19:37:02 +0200
+ Last update: Wed, 25 Oct 2017 21:44:33 +0200