diff options
author | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:08:55 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:08:55 -0700 |
commit | c86a3199caf050ef4af4ce5873ee7d6a27b501ab (patch) | |
tree | 47c42020587bffe014d52542bf8434b4a3a26683 /Util | |
parent | c7c9cd675bf6024a8f725c84fe22e17d3deb7a98 (diff) |
Dafny: added constructors
Diffstat (limited to 'Util')
-rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
-rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 | ||||
-rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
-rw-r--r-- | Util/vim/syntax/dafny.vim | 2 |
5 files changed, 6 insertions, 4 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 818d7dc3..b69a568a 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -30,7 +30,7 @@ ]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "function" "ghost" "var" "method" "unlimited"
+ "class" "datatype" "function" "ghost" "var" "method" "constructor" "unlimited"
"module" "imports" "static" "refines" "replaces" "by"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index a9353821..c620cc67 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -16,7 +16,7 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "datatype",
+ "class", "ghost", "static", "var", "method", "constructor", "datatype",
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"call", "if", "then", "else", "while", "invariant",
@@ -287,6 +287,7 @@ namespace Demo | "static"
| "var"
| "method"
+ | "constructor"
| "datatype"
| "assert"
| "assume"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index c37ea13c..654b5dcb 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -244,6 +244,7 @@ namespace DafnyLanguage case "case":
case "choose":
case "class":
+ case "constructor":
case "datatype":
case "decreases":
case "else":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index fccd3918..b29c054e 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -8,7 +8,7 @@ morekeywords={class,datatype,bool,nat,int,object,set,seq,array,array2,array3,%
function,unlimited,
ghost,var,static,refines,replaces,by,
- method,returns,module,imports,in,
+ method,constructor,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,allocated,choose,this,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 7727e1f6..fac7e6c7 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -5,7 +5,7 @@ syntax clear syntax case match -syntax keyword dafnyFunction function method +syntax keyword dafnyFunction function method constructor syntax keyword dafnyTypeDef class datatype syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat foreach while |