Dafny: changed triggers (which are never really used, anyhow) from having a special syntactic form to being just an attribute

Dafny: added "parallel" statement (so far, only parsing and resolving)
Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)

5 files changed, 6 insertions, 4 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index e352ad70..98006cca 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -37,7 +37,7 @@
         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"

-        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated"

+        "old" "forall" "exists" "new" "foreach" "parallel" "in" "this" "fresh" "allocated"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

    )

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index df0f22ee..8fc8bf4e 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -20,7 +20,7 @@ namespace Demo
           "assert", "assume", "new", "this", "object", "refines", "replaces", "by",

           "unlimited", "module", "imports",

           "if", "then", "else", "while", "invariant",

-          "break", "label", "return", "foreach", "havoc", "print",

+          "break", "label", "return", "foreach", "parallel", "havoc", "print",

           "returns", "requires", "ensures", "modifies", "reads", "decreases",

           "bool", "nat", "int", "false", "true", "null",

           "function", "free",

@@ -287,6 +287,7 @@ namespace Demo
           | "label"

           | "return"

           | "foreach"

+          | "parallel"

           | "havoc"

           | "print"

           | "returns"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 619f5f8d..5e61d2d6 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -272,6 +272,7 @@ namespace DafnyLanguage
                 case "null":

                 case "object":

                 case "old":

+                case "parallel":

                 case "print":

                 case "reads":

                 case "refines":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index ebcd7fb6..809c6fc4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -13,7 +13,7 @@
       % expressions

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

       % statements

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

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

       },

   literate=%

     {:}{$\colon$}1

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index e26227ed..4014e427 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -8,7 +8,7 @@ syntax case match
 syntax keyword dafnyFunction function method constructor
 syntax keyword dafnyTypeDef class datatype 
 syntax keyword dafnyConditional if then else match case 
-syntax keyword dafnyRepeat foreach while
+syntax keyword dafnyRepeat foreach while parallel
 syntax keyword dafnyStatement havoc assume assert return new print break label
 syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
 syntax keyword dafnyType bool nat int seq set object array array2 array3