Dafny:

* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files

3 files changed, 6 insertions, 6 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 20f4477b..75561d65 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -31,7 +31,7 @@
 

    `(,(dafny-regexp-opt '(

         "class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"

-        "module" "imports" "static"

+        "module" "imports" "static" "refines" "replaces" "by"

         "returns" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

         )) . font-lock-builtin-face)

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index dd44665a..5551cec0 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,13 +7,13 @@
 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,bool,int,object,set,seq,array,%

       function,unlimited,

-      ghost,var,static,

+      ghost,var,static,refines,replaces,by,

       method,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

       match,case,false,true,null,old,fresh,this,

       % statements

-      assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,return,foreach,

+      assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,

       },

   literate=%

     {:}{$\colon$}1

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 34379f6b..a6bccaa4 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -8,9 +8,9 @@ syntax case match
 syntax keyword dafnyFunction function method
 syntax keyword dafnyTypeDef class datatype 
 syntax keyword dafnyConditional if then else match case 
-syntax keyword dafnyRepeat for while
-syntax keyword dafnyStatement havoc assume assert return call new 
-syntax keyword dafnyKeyword var ghost returns null static this
+syntax keyword dafnyRepeat foreach while
+syntax keyword dafnyStatement havoc assume assert return call new print break label
+syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
 syntax keyword dafnyType int bool seq set
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
 syntax keyword dafnyOperator forall exists old fresh