Merge

7 files changed, 8 insertions, 33 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index bee88863..f3c48ab2 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4028,6 +4028,7 @@ namespace Microsoft.Dafny {
 

       var rhss = new List<AssignmentRhs>() { rhs };

       ProcessRhss(lhsBuilder, bLhss, lhss, rhss, builder, locals, etran);

+      builder.Add(CaptureState(tok));

     }

 

     void ProcessRhss(List<AssignToLhs> lhsBuilder, List<Bpl.IdentifierExpr/*may be null*/> bLhss,

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index b69a568a..e352ad70 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -36,8 +36,8 @@
         "invariant" "decreases"

         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

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

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

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

+        "old" "forall" "exists" "new" "foreach" "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 c620cc67..73c3891d 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -19,8 +19,8 @@ namespace Demo
           "class", "ghost", "static", "var", "method", "constructor", "datatype",

           "assert", "assume", "new", "this", "object", "refines", "replaces", "by",

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

-          "call", "if", "then", "else", "while", "invariant",

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

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

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

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

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

           "function", "free",

@@ -242,34 +242,12 @@ namespace Demo
                         | blockStatement

                         | expression + Semi

                         | "break" + Semi

-                        | "continue" + Semi

-                        | "return" + expression + Semi

                         | QualifiedName + ":=" + Rhs

 

                         | "var" + localVarStmt

 

-                        | "call" + identList + ":=" + FunctionExpression + Semi

-                        | "call" + FunctionExpression + Semi

                         | "assert" + expression + Semi

                         | "assume" + expression + Semi

-                        | "unshare" + expression + Semi

-                        | "acquire" + expression + Semi

-                        | "release" + expression + Semi

-                        | "downgrade" + expression + Semi

-                        | "free" + expression + Semi

-                        | "fold" + expression + Semi

-                        | "unfold" + expression + Semi

-                        | "reorder" + expression + installBounds + Semi

-                        | "reorder" + expression + Semi

-                        | "share" + expression + installBounds + Semi

-                        | "share" + expression + Semi

-                        | "fork" + identList + ":=" + FunctionExpression + Semi

-                        | "fork" + FunctionExpression + Semi

-                        | "join" + identList + ":=" + expression + Semi

-                        | "join" + expression + Semi

-                        | "send" + expression + Semi

-                        | "receive" + identList + ":=" + expression + Semi

-                        | "receive" + expression + Semi

 

                         ;

         Statements.Rule = MakeStarRule(Statements, null, Statement);

@@ -300,7 +278,6 @@ namespace Demo
           | "unlimited"

           | "module"

           | "imports"

-          | "call"

           | "if"

           | "then"

           | "else"

@@ -312,7 +289,6 @@ namespace Demo
           | "foreach"

           | "havoc"

           | "print"

-          | "use"

           | "returns"

           | "requires"

           | "ensures"

diff --git a/Util/VS2010/Dafny/StartDafny.bat b/Util/VS2010/Dafny/StartDafny.bat
index 2313e4d8..71dc149a 100644
--- a/Util/VS2010/Dafny/StartDafny.bat
+++ b/Util/VS2010/Dafny/StartDafny.bat
@@ -3,7 +3,7 @@ echo ---------- Starting ------------ < nul >> c:\tmp\doo.out
 time < nul >> c:\tmp\doo.out

 echo. < nul >> c:\tmp\doo.out

 

-"c:/boogie/Binaries/Dafny.exe" -nologo stdin.dfy -compile:0 -timeLimit:10 %* 2>> c:\tmp\doo.out

+"c:\boogie\Binaries\Dafny.exe" -nologo stdin.dfy -compile:0 -timeLimit:10 %* 2>> c:\tmp\doo.out

 

 time < nul >> c:\tmp\doo.out

 echo. < nul >> c:\tmp\doo.out

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 654b5dcb..619f5f8d 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -240,7 +240,6 @@ namespace DafnyLanguage
                 case "bool":

                 case "break":

                 case "by":

-                case "call":

                 case "case":

                 case "choose":

                 case "class":

@@ -288,7 +287,6 @@ namespace DafnyLanguage
                 case "this":

                 case "true":

                 case "unlimited":

-                case "use":

                 case "var":

                 case "while":

                 #endregion

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index b29c054e..ebcd7fb6 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,call,if,then,else,while,invariant,break,label,return,foreach,

+      assert,assume,print,new,havoc,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 fac7e6c7..e26227ed 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -9,7 +9,7 @@ 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 dafnyStatement havoc assume assert return call new print break label
+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
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant