diff options
| author |  Rustan Leino <unknown> | 2013-04-19 15:17:12 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-04-19 15:17:12 -0700 |
| commit | 7555f1e7dc8556b8ff1d2cab3c637b0556d1a946 (patch) | |
| tree | ec2a21d9316150b9d0e7e8bdb44628570115cdfc /Source/Dafny/Dafny.atg | |
| parent | 02f82c2a76acf6a9bbd3becfcfa0aebb57f14443 (diff) | |
Make semi-colon after datatype/codatatype declaration optional (in the future, it will not be allowed at all)
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index c71bf0bd..f3d0449a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -290,7 +290,13 @@ DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt> "=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
{ "|" DatatypeMemberDecl<ctors> }
- SYNC ";"
+ [ SYNC ";"
+ // This semi-colon used to be required, but it seems silly to have it.
+ // To stage the transition toward not having it at all, let's make it optional for now. Then,
+ // in a next big version of Dafny, including the following warning message:
+ // (. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
+ // And in a version after that, don't allow the semi-colon at all.
+ ]
(. if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
|