# HG changeset patch # User haftmann # Date 1174301976 -3600 # Node ID 365bce31e0519964ff6310aa618e9c24f0553f25 # Parent 01751f5b06578955d8072adceadc147afcc1fdcf dropped overwrite_warn diff -r 01751f5b0657 -r 365bce31e051 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Mon Mar 19 11:59:35 2007 +0100 +++ b/src/Pure/General/output.ML Mon Mar 19 11:59:36 2007 +0100 @@ -24,7 +24,6 @@ val priority: string -> unit val tracing: string -> unit val warning: string -> unit - val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list val debugging: bool ref val no_warnings: ('a -> 'b) -> 'a -> 'b val timing: bool ref @@ -151,19 +150,6 @@ fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f); -(* overwriting change with warning *) - -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); - - (* add_mode *) fun add_mode name (output, keyword, indent, raw) =