Dafny: removed allocated keyword, changed module import syntax. "opened" keyword is parsed but ignored.

1 files changed, 5 insertions, 4 deletions

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 4d8e2df1..7a124b74 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -19,7 +19,7 @@ namespace Demo
         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

           "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",

           "assert", "assume", "new", "this", "object", "refines",

-          "module", "imports", "as",

+          "module", "import", "as", "default", "opened",

           "if", "then", "else", "while", "invariant",

           "break", "label", "return", "parallel", "havoc", "print",

           "returns", "requires", "ensures", "modifies", "reads", "decreases",

@@ -28,7 +28,7 @@ namespace Demo
           "in", "forall", "exists",

           "seq", "set", "map", "multiset", "array", "array2", "array3",

           "match", "case",

-          "fresh", "allocated", "old", "choose", "where"

+          "fresh", "old", "choose", "where"

           );

 

         StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

@@ -276,7 +276,9 @@ namespace Demo
           | "object"

           | "refines"

           | "module"

-          | "imports"

+          | "import"

+          | "default"

+          | "opened"

           | "as"

           | "if"

           | "then"

@@ -318,7 +320,6 @@ namespace Demo
           | "match"

           | "case"

           | "fresh"

-          | "allocated"

           | "old"

           | "choose"

           | "where"