diff options
| author |  Rustan Leino <unknown> | 2014-02-13 20:00:42 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-13 20:00:42 -0800 |
| commit | 6897d8be8a9c5ebef140398f682021acfea393bb (patch) | |
| tree | f9837352353c4b539a0f2d90cee9ea756ff60942 /Util | |
| parent | 51406ab951236f10935bae6c653dad866b90f874 (diff) | |
Syntax highlighting for reals
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/dafny.vim | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 204dec45..c77fed74 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -42,7 +42,7 @@ "while" "print" "where"
"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)
+ `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "real" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 56b92a1e..d4624def 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -6,7 +6,7 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,type,iterator,
- bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
+ bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,
function,predicate,copredicate,
ghost,var,static,refines,
method,lemma,constructor,comethod,colemma,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index ad6839aa..06e1252e 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 syntax keyword dafnyKeyword var ghost returns yields null static this refines include -syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map +syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh syntax keyword dafnyBoolean true false |