summaryrefslogtreecommitdiff
path: root/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs')
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs10
1 files changed, 7 insertions, 3 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 81dd0dd1..9d6f0882 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -17,12 +17,13 @@ namespace Demo
StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
+ "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype",
+ "iterator", "type",
"assert", "assume", "new", "this", "object", "refines",
"module", "import", "as", "default", "opened",
"if", "then", "else", "while", "invariant",
- "break", "label", "return", "parallel", "print",
- "returns", "requires", "ensures", "modifies", "reads", "decreases",
+ "break", "label", "return", "yield", "parallel", "print",
+ "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
"function", "predicate", "copredicate", "free",
"in", "forall", "exists",
@@ -269,6 +270,7 @@ namespace Demo
| "datatype"
| "codatatype"
| "type"
+ | "iterator"
| "assert"
| "assume"
| "new"
@@ -288,9 +290,11 @@ namespace Demo
| "break"
| "label"
| "return"
+ | "yield"
| "parallel"
| "print"
| "returns"
+ | "yields"
| "requires"
| "ensures"
| "modifies"