Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to parallel syntax, other minor fixes

1 files changed, 2 insertions, 2 deletions

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index cfd8863f..74bfa65a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
 \usepackage{listings}

 

 \lstdefinelanguage{dafny}{

-  morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%

+  morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map%

       function,predicate,copredicate,

       ghost,var,static,refines,

       method,constructor,returns,module,imports,in,

@@ -13,7 +13,7 @@
       % expressions

       match,case,false,true,null,old,fresh,allocated,choose,this,

       % statements

-      assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,

+      assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,where

       },

   literate=%

     {:}{$\colon$}1