# HG changeset patch
# User wenzelm
# Date 961969526 -7200
# Node ID 62367f8fef02125ab9e7cd604b521909fb821048
# Parent  48ccddd9fdfe95c86645da322db71ad83ff24990
added change: 'a ref -> ('a -> 'a) -> unit;

diff -r 48ccddd9fdfe -r 62367f8fef02 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jun 23 14:00:43 2000 +0200
+++ b/src/Pure/library.ML	Sun Jun 25 23:45:26 2000 +0200
@@ -69,6 +69,7 @@
   val set: bool ref -> bool
   val reset: bool ref -> bool
   val toggle: bool ref -> bool
+  val change: 'a ref -> ('a -> 'a) -> unit
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
@@ -392,6 +393,8 @@
 fun reset flag = (flag := false; false);
 fun toggle flag = (flag := not (! flag); ! flag);
 
+fun change r f = r := f (! r);
+
 (*temporarily set flag, handling errors*)
 fun setmp flag value f x =
   let
@@ -725,7 +728,8 @@
     val tab_width = 8;
 
     fun untab (_, "\n") = (0, ["\n"])
-      | untab (pos, "\t") = let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end
+      | untab (pos, "\t") =
+          let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end
       | untab (pos, c) = (pos + 1, [c]);
   in
     if not (exists (equal "\t") chs) then chs