From be0690cd2e30b881acaad5c8610a0e550a0d55d6 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 6 Aug 2010 21:37:02 +0000
Subject: Dafny: Fixed VS 2010 mode to really include all Dafny keywords

---
 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'Util/VS2010/Dafny')

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"
-- 
cgit v1.2.3