summaryrefslogtreecommitdiff
path: root/Util/VS2010/Dafny
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-08-06 21:37:02 +0000
committerGravatar rustanleino <unknown>2010-08-06 21:37:02 +0000
commitbe0690cd2e30b881acaad5c8610a0e550a0d55d6 (patch)
treec6abe3e1594509f5e2e3741e8b41856abd0bfce4 /Util/VS2010/Dafny
parent7ecd4212a11290eafd9af6affe97dcccb1c0e4df (diff)
Dafny: Fixed VS 2010 mode to really include all Dafny keywords
Diffstat (limited to 'Util/VS2010/Dafny')
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs14
1 files changed, 11 insertions, 3 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 0a45490f..ba4fdcc0 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -13,7 +13,7 @@ namespace Demo
NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");
IdentifierTerminal ident = new IdentifierTerminal("Identifier");
- this.MarkReservedWords(
+ this.MarkReservedWords( // NOTE: these keywords must also appear once more below
"class", "ghost", "static", "var", "method", "datatype",
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
@@ -290,6 +290,12 @@ namespace Demo
| "new"
| "this"
| "object"
+ | "refines"
+ | "replaces"
+ | "by"
+ | "unlimited"
+ | "module"
+ | "imports"
| "call"
| "if"
| "then"
@@ -297,10 +303,12 @@ namespace Demo
| "while"
| "invariant"
| "break"
+ | "label"
| "return"
| "foreach"
- | "match"
- | "case"
+ | "havoc"
+ | "print"
+ | "use"
| "returns"
| "requires"
| "ensures"