Changes between Version 10 and Version 11 of NameSpaces

Timestamp:

2017-09-11 14:28:01 (8 years ago)

Author:

archibald

Comment:

--

NameSpaces

@@ -30 +30 @@
 
 {{{#!div style="background: #ffd; border: 3px ridge"
-namespaceClause := "NAMESPACE" {"$"} ident {":"ident}* { "-" {"$" ident { ":" ident }* { ident {":"ident}* }* }; 
+namespaceClause := "NAMESPACE" newNameSpaceClause  { "-" { existingNameSpaceClause }+ };
+newNameSpaceClause := { "$" ident { ":" ident }* | ident { ":" ident }* };
+existingNameSpaceClause := { "$" ident { ":" ident }* | ident { ":" ident }* };
 }}}