diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 8 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 6 |
2 files changed, 11 insertions, 3 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 {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 451cdd5c..aecb4ab1 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -414,8 +414,10 @@ bool IsLoopSpecOrAlternative() { Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(125); Get();}
- Expect(15);
+ if (la.kind == 15) {
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(125); Get();}
+ Get();
+ }
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
|