From e8cfbc8ad2c41ef051431b665c4c43e68cc0ff68 Mon Sep 17 00:00:00 2001 From: rustanleino 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Util/Emacs') 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" -- cgit v1.2.3