added setmp_noncritical;
authorwenzelm
Mon Jul 23 16:45:00 2007 +0200 (2007-07-23)
changeset 239327afee4bf89e8
parent 23931 4d82207fb251
child 23933 e1a792312472
added setmp_noncritical;
setmp: CRITICAL;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Jul 23 16:44:59 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jul 23 16:45:00 2007 +0200
     1.3 @@ -74,6 +74,7 @@
     1.4    val reset: bool ref -> bool
     1.5    val toggle: bool ref -> bool
     1.6    val change: 'a ref -> ('a -> 'a) -> unit
     1.7 +  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.8    val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.9  
    1.10    (*lists*)
    1.11 @@ -366,7 +367,7 @@
    1.12  fun change r f = r := f (! r);
    1.13  
    1.14  (*temporarily set flag during execution*)
    1.15 -fun setmp flag value f x =
    1.16 +fun setmp_noncritical flag value f x =
    1.17    let
    1.18      val orig_value = ! flag;
    1.19      val _ = flag := value;
    1.20 @@ -374,6 +375,8 @@
    1.21      val _ = flag := orig_value;
    1.22    in release result end;
    1.23  
    1.24 +fun setmp flag value f x = CRITICAL (fn () => setmp_noncritical flag value f x);
    1.25 +
    1.26  
    1.27  
    1.28  (** lists **)