--- a/src/Pure/General/output.ML Mon Nov 13 15:43:13 2006 +0100
+++ b/src/Pure/General/output.ML Mon Nov 13 15:43:14 2006 +0100
@@ -24,6 +24,7 @@
val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
+ val change_warn: ('b -> 'a -> bool) -> ('a -> 'b -> 'b) -> ('a -> string) -> 'a -> 'b -> 'b
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
val show_debug_msgs: bool ref
@@ -152,6 +153,12 @@
fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
+(* overwriting change with warning *)
+
+fun change_warn ex upd msg x xs =
+ (if ex xs x then warning (msg x) else (); upd x xs);
+
+
(* AList operations *)
fun overwrite (al, p as (key, _)) =