diff options
| author |  leino <unknown> | 2014-08-21 21:03:52 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-21 21:03:52 -0700 |
| commit | 900c42823f0661107543716a247bec22f01cd9cc (patch) | |
| tree | 13fdda07d14827c2bad6fd71d4180cf1d0084d56 /Util | |
| parent | 81669a1d8bb2e36d86464708bb234e7920776ae6 (diff) | |
Changed syntax of derived types to "newtype"
Added parsing of constraints (beyond parsing is yet to come)
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 d589fb78..6482ff28 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -30,7 +30,7 @@ ]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "codatatype" "type" "iterator"
+ "class" "datatype" "codatatype" "newtype" "type" "iterator"
"trait" "extends"
"function" "predicate" "copredicate"
"ghost" "var" "method" "lemma" "constructor" "colemma"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 40b994ba..dc0d18c7 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,trait,extends,
+ morekeywords={class,datatype,codatatype,newtype,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 58820c0f..92c0b079 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 trait extends +syntax keyword dafnyTypeDef class datatype codatatype newtype 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 |