# HG changeset patch
# User wenzelm
# Date 1185201900 -7200
# Node ID 7afee4bf89e8ad1c57a73e4e5a5a19f5d0054bf6
# Parent  4d82207fb25146e8de7b22b1ab609f4fc1f38754
added setmp_noncritical;
setmp: CRITICAL;

diff -r 4d82207fb251 -r 7afee4bf89e8 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jul 23 16:44:59 2007 +0200
+++ b/src/Pure/library.ML	Mon Jul 23 16:45:00 2007 +0200
@@ -74,6 +74,7 @@
   val reset: bool ref -> bool
   val toggle: bool ref -> bool
   val change: 'a ref -> ('a -> 'a) -> unit
+  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
@@ -366,7 +367,7 @@
 fun change r f = r := f (! r);
 
 (*temporarily set flag during execution*)
-fun setmp flag value f x =
+fun setmp_noncritical flag value f x =
   let
     val orig_value = ! flag;
     val _ = flag := value;
@@ -374,6 +375,8 @@
     val _ = flag := orig_value;
   in release result end;
 
+fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
+
 
 
 (** lists **)