diff options
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 1 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/dafny.vim | 2 |
4 files changed, 3 insertions, 4 deletions
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 4a610c73..b019db0a 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -261,7 +261,6 @@ namespace DafnyLanguage case "break":
case "calc":
case "case":
- case "choose":
case "class":
case "codatatype":
case "colemma":
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index c59de6ed..7075a30d 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -38,7 +38,7 @@ "invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
- "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
+ "assert" "assume" "break" "then" "else" "if" "label" "return" "yield"
"while" "print" "where"
"old" "forall" "exists" "new" "calc" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index d8d4ad96..f282fa7c 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ returns,yields,abstract,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
- match,case,false,true,null,old,fresh,choose,this,
+ match,case,false,true,null,old,fresh,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
where,calc
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 414b5fdc..a4ef0d1a 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -15,7 +15,7 @@ syntax keyword dafnyStatement assume assert return yield new print break label w syntax keyword dafnyKeyword var ghost returns yields null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant -syntax keyword dafnyOperator forall exists old fresh choose +syntax keyword dafnyOperator forall exists old fresh syntax keyword dafnyBoolean true false syntax region dafnyString start=/"/ skip=/\\"/ end=/"/ |