diff options
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 1 | ||||
| -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 |
4 files changed, 4 insertions, 3 deletions
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index f3c6fc4e..db4d0858 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -304,6 +304,7 @@ namespace DafnyLanguage case "function":
case "ghost":
case "if":
+ case "imap":
case "import":
case "in":
case "include":
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 656fdb06..80186e12 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -46,7 +46,7 @@ "match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '(
"bool" "char" "int" "nat" "real"
- "set" "multiset" "seq" "string" "map"
+ "set" "multiset" "seq" "string" "map" "imap"
"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 0b9348ea..19eb544a 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,char,nat,int,real,object,set,multiset,seq,string,map,array,array2,array3,
+ bool,char,nat,int,real,object,set,multiset,seq,string,map,imap,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 a98d1e2f..cbbc1e76 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 char nat int real set multiset seq string map object array array2 array3 +syntax keyword dafnyType bool char nat int real set multiset seq string map imap 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 |