From e5fcbeda373f505f4ebfd29cafe776d9ec7b8db5 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 8 May 2010 02:19:17 +0000
Subject: Dafny: Previously, a "use" function was one whose definition was
 applied only in limited ways, namely when the function was uttered in a
 program (possibly in a "use" statement).  Now, recursive functions are always
 limited, unless declared with the new modifier "unlimited".  Non-recursive
 functions are always unlimited.  Also new is that only function calls within
 the same SCC of the call graph use the limited form of the callee. The "use"
 modifier is no longer supported.  The "use" statement is still supported, now
 for both limited and unlimited functions; but it's probably better and easier
 to just explicitly mention a function in an assertion, if needed.

---
 Util/Emacs/dafny-mode.el | 2 +-
 Util/latex/dafny.sty     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 34fc96f2..7b5de59a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
 ]\\)*" . font-lock-comment-face)
 
    `(,(dafny-regexp-opt '(
-        "class" "datatype" "function" "frame" "ghost" "var" "method"
+        "class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"
         "module" "imports" "static"
         "returns" "requires" "ensures" "modifies" "reads" "free"
         "invariant" "decreases"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 2b9918f9..1f891a71 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,9 +6,9 @@
 
 \lstdefinelanguage{dafny}{
   morekeywords={class,datatype,bool,int,object,set,seq,%
-      function,returns,
+      function,unlimited,
       ghost,var,static,
-      method,module,imports,in,
+      method,returns,module,imports,in,
       requires,modifies,ensures,reads,decreases,free,
       % expressions
       match,case,false,true,null,old,fresh,this,
-- 
cgit v1.2.3