summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-07-06 23:08:37 +0000
committerGravatar rustanleino <unknown>2010-07-06 23:08:37 +0000
commit0cd554f0b5c748b76263dac4b4ff8bce559339e4 (patch)
tree5662d1b37ebd47901950a1212e408d765a26690a /Util
parenta2844f2e24d7e90ba8fc2f0307a02d6ba68f4c7f (diff)
Dafny:
* changed rule about scoping of out-parameters * added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
Diffstat (limited to 'Util')
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty4
-rw-r--r--Util/vim/syntax/dafny.vim6
3 files changed, 6 insertions, 6 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 20f4477b..75561d65 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -31,7 +31,7 @@
`(,(dafny-regexp-opt '(
"class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"
- "module" "imports" "static"
+ "module" "imports" "static" "refines" "replaces" "by"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index dd44665a..5551cec0 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,13 +7,13 @@
\lstdefinelanguage{dafny}{
morekeywords={class,datatype,bool,int,object,set,seq,array,%
function,unlimited,
- ghost,var,static,
+ ghost,var,static,refines,replaces,by,
method,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,this,
% statements
- assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,return,foreach,
+ assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 34379f6b..a6bccaa4 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -8,9 +8,9 @@ syntax case match
syntax keyword dafnyFunction function method
syntax keyword dafnyTypeDef class datatype
syntax keyword dafnyConditional if then else match case
-syntax keyword dafnyRepeat for while
-syntax keyword dafnyStatement havoc assume assert return call new
-syntax keyword dafnyKeyword var ghost returns null static this
+syntax keyword dafnyRepeat foreach while
+syntax keyword dafnyStatement havoc assume assert return call new print break label
+syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
syntax keyword dafnyType int bool seq set
syntax keyword dafnyLogic requires ensures modifies reads decreases invariant
syntax keyword dafnyOperator forall exists old fresh