From 66939a686e115c00e9cb6824e7c5a2dadc85a8df Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 14 Jan 2010 22:20:49 +0000
Subject: Dafny:  * Allow (and currently ignore) "ghost" modifier.  * Fixed bug
 in boxing.  * Check for div-by-zero error for modulo operator.  * Improved
 emacs and latex modes.

---
 Util/latex/dafny.sty | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'Util/latex')

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index f334e770..f88c3b54 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,9 +7,9 @@
 \lstdefinelanguage{dafny}{
   morekeywords={class,datatype,bool,int,object,set,seq,%
       function,returns,
-      var,
+      ghost,var,
       method,in,
-      requires,modifies,ensures,reads,free,
+      requires,modifies,ensures,reads,decreases,free,
       % expressions
       match,case,false,true,null,old,fresh,this,
       % statements
@@ -20,15 +20,18 @@
     {::}{$\bullet$}2
     {:=}{$:$$=$}2
     {!}{$\lnot$}1
-    {!!}{$\nparallel$}1
+    {!!}{$\not\cap$}1
     {==}{$=$}1
     {!=}{$\neq$}1
     {&&}{$\land$}1
     {||}{$\lor$}1
     {<=}{$\le$}1
     {=>}{$\ge$}1
+    % the following isn't actually Dafny, but it gives the option to produce nicer latex
+    {|=>}{$\Rightarrow$}2
     {<=set}{$\subseteq$}1
     {+set}{$\cup$}1
+    {*set}{$\cap$}1
     {==>}{$\Longrightarrow$}3 
     {<==>}{$\Longleftrightarrow$}4 
     {forall}{$\forall$}1
@@ -38,6 +41,7 @@
     % the following isn't actually Dafny, but it gives the option to produce nicer latex
     {<<}{$\langle$}1
     {>>}{$\rangle$}1
+    {...}{$\ldots$}1
     {\\alpha}{$\alpha$}1
     {\\beta}{$\beta$}1
     {\\gamma}{$\gamma$}1
-- 
cgit v1.2.3