improved inc, dec;
authorwenzelm
Wed, 16 Apr 1997 18:16:02 +0200
changeset 2958 7837471d2f27
parent 2957 d35fca99b3be
child 2959 071bfb16586f
improved inc, dec; added set_ap;
src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Apr 16 18:15:32 1997 +0200
+++ b/src/Pure/library.ML	Wed Apr 16 18:16:02 1997 +0200
@@ -142,6 +142,15 @@
 fun reset flag = (flag := false; false);
 fun toggle flag = (flag := not (! flag); ! flag);
 
+fun set_ap flag value f x =
+  let
+    val orig_value = ! flag;
+    fun return y = (flag := orig_value; y);
+  in
+    flag := value;
+    return (f x handle exn => (return (); raise exn))
+  end;
+
 
 
 (** lists **)
@@ -322,8 +331,8 @@
 
 (** integers **)
 
-fun inc i = i := ! i + 1;
-fun dec i = i := ! i - 1;
+fun inc i = (i := ! i + 1; ! i);
+fun dec i = (i := ! i - 1; ! i);
 
 
 (* lists of integers *)