diff options
author | Jason Koenig <unknown> | 2012-07-30 11:43:28 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2012-07-30 11:43:28 -0700 |
commit | ded134088845e37125e3d38929d37c5a9424518a (patch) | |
tree | d31c6e66edd3641d25550cec2da7ba2fb732bcf0 /Util | |
parent | 096908b4bd4be630d7adf7448dea7eeb03e83d47 (diff) |
Dafny: removed allocated keyword, changed module import syntax. "opened" keyword is parsed but ignored.
Diffstat (limited to 'Util')
-rw-r--r-- | Util/Emacs/dafny-mode.el | 4 | ||||
-rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 9 | ||||
-rw-r--r-- | Util/latex/dafny.sty | 4 | ||||
-rw-r--r-- | Util/vim/syntax/dafny.vim | 4 |
4 files changed, 11 insertions, 10 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index e4a8c5d0..0b64a775 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -32,13 +32,13 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
"ghost" "var" "method" "constructor"
- "module" "imports" "static" "refines"
+ "module" "import" "default" "as" "opened" "static" "refines"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print" "where"
- "old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"
+ "old" "forall" "exists" "new" "parallel" "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 4d8e2df1..7a124b74 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -19,7 +19,7 @@ namespace Demo this.MarkReservedWords( // NOTE: these keywords must also appear once more below
"class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
"assert", "assume", "new", "this", "object", "refines",
- "module", "imports", "as",
+ "module", "import", "as", "default", "opened",
"if", "then", "else", "while", "invariant",
"break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
@@ -28,7 +28,7 @@ namespace Demo "in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
- "fresh", "allocated", "old", "choose", "where"
+ "fresh", "old", "choose", "where"
);
StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
@@ -276,7 +276,9 @@ namespace Demo | "object"
| "refines"
| "module"
- | "imports"
+ | "import"
+ | "default"
+ | "opened"
| "as"
| "if"
| "then"
@@ -318,7 +320,6 @@ namespace Demo | "match"
| "case"
| "fresh"
- | "allocated"
| "old"
| "choose"
| "where"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 74bfa65a..9ce6c3e1 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -8,10 +8,10 @@ morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map%
function,predicate,copredicate,
ghost,var,static,refines,
- method,constructor,returns,module,imports,in,
+ method,constructor,returns,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
- match,case,false,true,null,old,fresh,allocated,choose,this,
+ match,case,false,true,null,old,fresh,choose,this,
% statements
assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,where
},
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 37ec7be0..6023830c 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -6,14 +6,14 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate method constructor -syntax keyword dafnyTypeDef class datatype codatatype type +syntax keyword dafnyTypeDef class datatype codatatype type module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel syntax keyword dafnyStatement havoc assume assert return new print break label where syntax keyword dafnyKeyword var ghost returns null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant -syntax keyword dafnyOperator forall exists old fresh allocated choose +syntax keyword dafnyOperator forall exists old fresh choose syntax keyword dafnyBoolean true false syntax region dafnyString start=/"/ skip=/\\"/ end=/"/ |