diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 13:23:20 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 13:23:20 -0800 |
| commit | a95e7d5e1172d19df14623014ead072924e1af4c (patch) | |
| tree | 626706eca3463a60a89a3afeaaadfde08a450e4f /Util | |
| parent | c7b6946ca6368f6ec307802b82b4e44a6cab83cd (diff) | |
Dafny: added predicates
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 3811e2c0..56b56000 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" "type" "function" "ghost" "var" "method" "constructor" "unlimited"
+ "class" "datatype" "type" "function" "predicate" "ghost" "var" "method" "constructor" "unlimited"
"module" "imports" "static" "refines"
"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 e35383b0..41923a98 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -24,7 +24,7 @@ namespace Demo "break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
- "function", "free",
+ "function", "predicate", "free",
"in", "forall", "exists",
"seq", "set", "multiset", "array", "array2", "array3",
"match", "case",
@@ -301,6 +301,7 @@ namespace Demo | "true"
| "null"
| "function"
+ | "predicate"
| "free"
| "in"
| "forall"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 78c5f8d9..650c01bd 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -272,6 +272,7 @@ namespace DafnyLanguage case "object":
case "old":
case "parallel":
+ case "predicate":
case "print":
case "reads":
case "refines":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 28759fd4..b23e2dc4 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -6,7 +6,7 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
- function,unlimited,
+ function,predicate,unlimited,
ghost,var,static,refines,
method,constructor,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index faac0cbb..37038f35 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 constructor +syntax keyword dafnyFunction function predicate method constructor syntax keyword dafnyTypeDef class datatype type syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel |