Changes between Version 16 and Version 17 of NameSpaces


Ignore:
Timestamp:
2017-09-11 16:18:59 (8 years ago)
Author:
archibald
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • NameSpaces

    v16 v17  
    3131{{{#!div style="background: #ffd; border: 3px ridge" 
    3232namespaceClause := "NAMESPACE" newNameSpaceClause  { "-" { existingNameSpaceClause }+ }; 
    33 [[Image(namespaceClause.png,width=100%)]] 
     33[[Image(namespaceClause.png,width=98%)]] 
    3434 
    3535newNameSpaceClause := { "$" ident { ":" ident }* | ident { ":" ident }* }; 
    36 [[Image(newNamespaceClause.png,width=100%)]] 
     36[[Image(newNamespaceClause.png,width=98%)]] 
    3737 
    3838existingNameSpaceClause := { "$" ident { ":" ident }* | ident { ":" ident }* };[[BR]] 
    39 [[Image(existingNamespaceClause.png,width=100%)]] 
     39[[Image(existingNamespaceClause.png,width=98%)]] 
    4040}}}