From 77143c833cbb14a20c704fb60fc28dd94edb44eb Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Fri, 18 Jul 2014 21:16:40 +0300 Subject: added trait feature: -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods --- Util/Emacs/dafny-mode.el | 1 + Util/latex/dafny.sty | 2 +- Util/vim/dafny.vim | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) (limited to 'Util') diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 6c59c50a..d589fb78 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -31,6 +31,7 @@ `(,(dafny-regexp-opt '( "class" "datatype" "codatatype" "type" "iterator" + "trait" "extends" "function" "predicate" "copredicate" "ghost" "var" "method" "lemma" "constructor" "colemma" "abstract" "module" "import" "default" "as" "opened" "static" "refines" diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 785cf6f1..40b994ba 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings} \lstdefinelanguage{dafny}{ - morekeywords={class,datatype,codatatype,type,iterator, + morekeywords={class,datatype,codatatype,type,iterator,trait,extends, bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map, function,predicate,copredicate, ghost,var,static,refines, diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index c706ac5f..58820c0f 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -7,7 +7,7 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate syntax keyword dafnyMethod method lemma constructor colemma -syntax keyword dafnyTypeDef class datatype codatatype type iterator +syntax keyword dafnyTypeDef class datatype codatatype type iterator trait extends syntax keyword dafnyModule abstract module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while -- cgit v1.2.3