From b06749500528f113ace48fd2fd7d0412c84a9c78 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 6 Aug 2013 18:37:40 -0700
Subject: Removed old keyword "choose"

---
 Source/DafnyExtension/TokenTagger.cs | 1 -
 Util/Emacs/dafny-mode.el             | 2 +-
 Util/latex/dafny.sty                 | 2 +-
 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=/"/
-- 
cgit v1.2.3