From 172554c51fad4092f2b4e52a921ad0e86fa67ca6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 6 Mar 2013 15:09:04 -0800
Subject: Renamed "parallel" statement to "forall" statement, and made the
 parentheses around the bound variables optional.

---
 Util/Emacs/dafny-mode.el                          | 2 +-
 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 +--
 Util/latex/dafny.sty                              | 4 ++--
 Util/vim/dafny.vim                                | 2 +-
 4 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d1bdcf12..b043150c 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
    `(,(dafny-regexp-opt '(
         "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
         "while" "print" "where"
-        "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"
+        "old" "forall" "exists" "new" "calc" "in" "this" "fresh"
         "match" "case" "false" "true" "null")) . font-lock-keyword-face)
    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "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 dd910820..fe7c6638 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -22,7 +22,7 @@ namespace Demo
           "assert", "assume", "new", "this", "object", "refines",
           "abstract", "module", "import", "as", "default", "opened",
           "if", "then", "else", "while", "invariant",
-          "break", "label", "return", "yield", "parallel", "print",
+          "break", "label", "return", "yield", "print",
           "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
           "bool", "nat", "int", "false", "true", "null",
           "function", "predicate", "copredicate", "free",
@@ -293,7 +293,6 @@ namespace Demo
           | "label"
           | "return"
           | "yield"
-          | "parallel"
           | "calc"
           | "print"
           | "returns"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 4a3f6dbc..e3007b75 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -16,12 +16,13 @@
       match,case,false,true,null,old,fresh,choose,this,
       % statements
       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
-      parallel,where,calc
+      where,calc
       },
   literate=%
     {:}{$\colon$}1
     {::}{$\bullet$}2
     {:=}{$:$$=$}2
+    {:|}{${:}\!\!|$}2
     {!}{$\lnot$}1
     {!!}{$\not\cap$}1
     {==}{$=$}1
@@ -31,7 +32,6 @@
     {<=}{$\le$}1
     {>=}{$\ge$}1
     % the following isn't actually Dafny, but it gives the option to produce nicer latex
-    {|=>}{$\Rightarrow$}2
     {<=set}{$\subseteq$}1
     {+set}{$\cup$}1
     {*set}{$\cap$}1
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index b329f0f7..31f27c51 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -10,7 +10,7 @@ syntax keyword method constructor comethod
 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 parallel
+syntax keyword dafnyRepeat while
 syntax keyword dafnyStatement assume assert return yield new print break label where calc
 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
-- 
cgit v1.2.3