From cd206ac033a1e369277f824dd3a13eca32f0396c Mon Sep 17 00:00:00 2001 From: Rustan Leino 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Util/Emacs') 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) ) -- cgit v1.2.3