summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-08-06 18:37:40 -0700
committerGravatar Rustan Leino <unknown>2013-08-06 18:37:40 -0700
commitb06749500528f113ace48fd2fd7d0412c84a9c78 (patch)
tree9b54dfe7c5d412c2f56e0e5bdefe62501ad4d5f2
parentb40564833ddf8408d446d5b2c0ba376dbea51c68 (diff)
Removed old keyword "choose"
-rw-r--r--Source/DafnyExtension/TokenTagger.cs1
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/dafny.vim2
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=/"/