diff options
| author |  leino <unknown> | 2014-10-20 17:08:46 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-20 17:08:46 -0700 |
| commit | 82edb1b179916ee61655ab7e425a17ab5145fac8 (patch) | |
| tree | d921e9e5a05a5eafbf04e77800a06b73bfed6c6f /Util | |
| parent | 963c6622a33dcff4875dbd44be1702cb979c917c (diff) | |
Added types "char" and "string" (the latter being a synonym for "seq<char>").
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 4 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/dafny.vim | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index ab794e2f..656fdb06 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -45,8 +45,8 @@ "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '(
- "bool" "int" "nat" "real"
- "set" "multiset" "seq" "map"
+ "bool" "char" "int" "nat" "real"
+ "set" "multiset" "seq" "string" "map"
"object" "array" "array2" "array3")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index dc0d18c7..0b9348ea 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -6,7 +6,7 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,
- bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,
+ bool,char,nat,int,real,object,set,multiset,seq,string,map,array,array2,array3,
function,predicate,copredicate,
ghost,var,static,refines,
method,lemma,constructor,colemma,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 92c0b079..a98d1e2f 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -13,7 +13,7 @@ syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while syntax keyword dafnyStatement assume assert return yield new print break label where calc modify syntax keyword dafnyKeyword var ghost returns yields null static this refines include -syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map +syntax keyword dafnyType bool char nat int real set multiset seq string map object array array2 array3 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh syntax keyword dafnyBoolean true false |