# HG changeset patch
# User haftmann
# Date 1127291526 -7200
# Node ID b2ce48df4d4c7c022844a1a27a407a94c9435ce2
# Parent  9b089c63f08828a8622351dc5c75b4f9243e7ea3
added update_warn

diff -r 9b089c63f088 -r b2ce48df4d4c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Sep 21 00:07:32 2005 +0200
+++ b/src/Pure/General/output.ML	Wed Sep 21 10:32:06 2005 +0200
@@ -35,6 +35,8 @@
   val assert: bool -> string -> unit
   val deny: bool -> string -> unit
   val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
+  val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b)
+    -> ('a * 'b) list -> ('a * 'b) list
   val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   datatype 'a error = Error of string | OK of 'a
   val get_error: 'a error -> string option
@@ -159,6 +161,12 @@
         | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
   in asl l end;
 
+fun overwrite (al, p as (key, _)) =
+  let fun over ((q as (keyi, _)) :: pairs) =
+            if keyi = key then p :: pairs else q :: (over pairs)
+        | over [] = [p]
+  in over al end;
+
 fun overwrite_warn (args as (alist, (a, _))) msg =
  (if is_none (AList.lookup (op =) alist a) then () else warning msg;
   overwrite args);