--- 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);