diff options
| author |  Bryan Parno <parno@microsoft.com> | 2013-12-10 13:41:50 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2013-12-10 13:41:50 -0800 |
| commit | 195097dc1353946f524f2518453bd356a09f6681 (patch) | |
| tree | ffeb46c86abb50fa8f2df26dddd9526880f39bd1 /Util | |
| parent | 982e64871949040b3d766c4d36f9ccdf5f506f7a (diff) | |
Add support for the "include" keyword, which accepts a (possibly relative) path
to another Dafny file. That file's functions and methods are included but not checked.
This is intended to support incremental verification on a per-file basis.
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 7075a30d..2fe109f5 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -35,7 +35,7 @@ "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma"
"abstract" "module" "import" "default" "as" "opened" "static" "refines"
"returns" "yields" "requires" "ensures" "modifies" "reads" "free"
- "invariant" "decreases"
+ "invariant" "decreases" "include"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "then" "else" "if" "label" "return" "yield"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index f282fa7c..83c2bf75 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -11,7 +11,7 @@ ghost,var,static,refines,
method,lemma,constructor,comethod,colemma,
returns,yields,abstract,module,import,default,opened,as,in,
- requires,modifies,ensures,reads,decreases,free,
+ requires,modifies,ensures,reads,decreases,free,include
% expressions
match,case,false,true,null,old,fresh,this,
% statements
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index a4ef0d1a..ad6839aa 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -12,7 +12,7 @@ syntax keyword 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 -syntax keyword dafnyKeyword var ghost returns yields null static this refines +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 dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh |