diff options
| author |  rustanleino <unknown> | 2010-07-06 23:08:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-07-06 23:08:37 +0000 |
| commit | ef3e335bf3caf7c43a6ba915ea4ed4edb0977ed6 (patch) | |
| tree | 1a3542a2ba19f38da22c1991b12ff4bcfeadae90 /Util/latex | |
| parent | 1a7842037a68d67db494b060dc73cad60aa31332 (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/latex')
| -rw-r--r-- | Util/latex/dafny.sty | 4 |
1 files changed, 2 insertions, 2 deletions
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
|