tuned setmp;
authorwenzelm
Thu Jan 19 21:22:17 2006 +0100 (2006-01-19)
changeset 18712836520885b8f
parent 18711 cf020c54e2f5
child 18713 cf777b9788b5
tuned setmp;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Jan 19 21:22:16 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Jan 19 21:22:17 2006 +0100
     1.3 @@ -471,15 +471,14 @@
     1.4  
     1.5  fun change r f = r := f (! r);
     1.6  
     1.7 -(*temporarily set flag, handling exceptions*)
     1.8 +(*temporarily set flag during execution*)
     1.9  fun setmp flag value f x =
    1.10    let
    1.11      val orig_value = ! flag;
    1.12 -    fun return y = (flag := orig_value; y);
    1.13 -  in
    1.14 -    flag := value;
    1.15 -    return (f x handle exn => (return (); raise exn))
    1.16 -  end;
    1.17 +    val _ = flag := value;
    1.18 +    val result = capture f x;
    1.19 +    val _ = flag := orig_value;
    1.20 +  in release result end;
    1.21  
    1.22  
    1.23  (* conditional execution *)