summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-12-11 14:04:16 -0800
committerGravatar Rustan Leino <unknown>2013-12-11 14:04:16 -0800
commit376de738788587074764afae8eb096e589402ef2 (patch)
tree24efb4c847d5a1c4e79d2f73e304b733527c86c4 /Util
parent863f701784a8aa0a4d7fd625620441cd64e38bac (diff)
parentec7c748e75361694d704b2eb6f93df920c39d6e4 (diff)
Merge
Diffstat (limited to 'Util')
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/dafny.vim2
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