# 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