# HG changeset patch
# User wenzelm
# Date 1220818786 -7200
# Node ID 0435d23deccc2fcd11dd8863011a93492335df09
# Parent  5205f7979b4fa61f818c864ec5218034d4cc9042
added change_result;

diff -r 5205f7979b4f -r 0435d23deccc src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Sep 07 22:19:42 2008 +0200
+++ b/src/Pure/library.ML	Sun Sep 07 22:19:46 2008 +0200
@@ -63,6 +63,7 @@
   val reset: bool ref -> bool
   val toggle: bool ref -> bool
   val change: 'a ref -> ('a -> 'a) -> unit
+  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
   val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
@@ -329,6 +330,7 @@
 fun toggle flag = (flag := not (! flag); ! flag);
 
 fun change r f = r := f (! r);
+fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
 
 (*temporarily set flag during execution*)
 fun setmp_noncritical flag value f x =