diff options
author | Rustan Leino <leino@microsoft.com> | 2011-11-21 22:40:44 -0800 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-11-21 22:40:44 -0800 |
commit | 166c105b43515bfdbde52514fa9c16ffd61eea25 (patch) | |
tree | 1d01cd5c3147c98ccc03e43a6659574f5c3f81c7 /Util/VS2010 | |
parent | b07cff8fc3c732986c42b31226f0d7b06ed55886 (diff) |
Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
Diffstat (limited to 'Util/VS2010')
-rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 557beb32..f2924420 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,7 +17,7 @@ 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",
+ "class", "ghost", "static", "var", "method", "constructor", "datatype", "type",
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"if", "then", "else", "while", "invariant",
@@ -267,6 +267,7 @@ namespace Demo | "method"
| "constructor"
| "datatype"
+ | "type"
| "assert"
| "assume"
| "new"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index e8e94e17..23c71d45 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -287,6 +287,7 @@ namespace DafnyLanguage case "then":
case "this":
case "true":
+ case "type":
case "unlimited":
case "var":
case "while":
|