diff options
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 80186e12..e4bf845b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -33,7 +33,7 @@ "class" "trait" "datatype" "codatatype" "newtype" "type" "iterator"
"function" "predicate" "copredicate"
"var" "method" "constructor" "lemma" "colemma"
- "ghost" "static" "abstract"
+ "ghost" "static" "protected" "abstract"
"module" "import" "default" "as" "opened"
"include"
"extends" "refines" "returns" "yields"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 19eb544a..10896434 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -8,7 +8,7 @@ morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,
bool,char,nat,int,real,object,set,multiset,seq,string,map,imap,array,array2,array3,
function,predicate,copredicate,
- ghost,var,static,refines,
+ ghost,var,static,protected,refines,
method,lemma,constructor,colemma,
returns,yields,abstract,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,include,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index cbbc1e76..65d7165f 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -12,7 +12,7 @@ syntax keyword dafnyModule abstract module import opened as default 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 dafnyKeyword var ghost returns yields null static protected this refines include 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 |