diff options
| author |  leino <unknown> | 2014-12-02 18:06:50 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-12-02 18:06:50 -0800 |
| commit | 5bb3834b184f7f2a2f9d3d5b1d8acf2de6b3b8fc (patch) | |
| tree | ebe8eaaff6a68d0488ef713034c2bb6c9d380669 /Source/Dafny/Dafny.atg | |
| parent | 682a34e72274aff3ef4ebcbe54244d1c2ca0ba2f (diff) | |
Fixed parser lookahead bug that had caused an infinite loop.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 29e33b35..132ec4d1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -234,7 +234,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { }
bool IsNotEndOfCase() {
- return la.kind != _rbrace && la.kind != _case;
+ return la.kind != _EOF && la.kind != _rbrace && la.kind != _case;
}
/*--------------------------------------------------------------------------*/
@@ -1603,8 +1603,13 @@ CaseStatement<out MatchCaseStmt/*!*/ c> }
")" ]
"=>"
+ SYNC /* this SYNC and the one inside the loop below are used to avoid problems with the IsNotEndOfCase test. The SYNC will
+ * skip until the next symbol that can legally occur here, which is either the beginning of a Stmt or whatever is allowed
+ * to follow the CaseStatement.
+ */
{ IF(IsNotEndOfCase()) /* This is a little sketchy. It would be nicer to be able to write IF(la is start-symbol of Stmt), but Coco doesn't allow that */
Stmt<body>
+ SYNC /* see comment about SYNC above */
}
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
|