From cd206ac033a1e369277f824dd3a13eca32f0396c Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 3 Apr 2014 18:28:56 -0700
Subject: Added "modify" statement. In a frame govered by a ghost context,
 ignore explicit mentions of `g if g is a ghost field.

---
 Util/Emacs/dafny-mode.el | 2 +-
 Util/latex/dafny.sty     | 2 +-
 Util/vim/dafny.vim       | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d663665b..6c59c50a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
    `(,(dafny-regexp-opt '(
         "assert" "assume" "break" "then" "else" "if" "label" "return" "yield"
         "while" "print" "where"
-        "old" "forall" "exists" "new" "calc" "in" "this" "fresh"
+        "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"
         "match" "case" "false" "true" "null")) . font-lock-keyword-face)
    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "real" "object" "set" "seq")) . font-lock-type-face)
    )
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 361b72d2..785cf6f1 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -16,7 +16,7 @@
       match,case,false,true,null,old,fresh,this,
       % statements
       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
-      where,calc
+      where,calc,modify
       },
   literate=%
     {:}{$\colon$}1
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index f533a621..d6e6bac5 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -11,7 +11,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword abstract module import opened as default
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while
-syntax keyword dafnyStatement assume assert return yield new print break label where calc
+syntax keyword dafnyStatement assume assert return yield new print break label where calc modify
 syntax keyword dafnyKeyword var ghost returns yields null static this refines include
 syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
-- 
cgit v1.2.3