dropped Output.update_warn
authorhaftmann
Wed Jan 31 16:05:13 2007 +0100 (2007-01-31)
changeset 222206dc8d0dca678
parent 22219 61b5bab471ce
child 22221 8a8aa6114a89
dropped Output.update_warn
src/HOL/Tools/sat_solver.ML
src/Pure/General/output.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:13 2007 +0100
     1.3 @@ -357,8 +357,13 @@
     1.4  
     1.5  	(* string * solver -> unit *)
     1.6  
     1.7 -	fun add_solver (name, new_solver) =
     1.8 -		(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers));
     1.9 +    fun add_solver (name, new_solver) =
    1.10 +      let
    1.11 +        val the_solvers = !solvers;
    1.12 +        val _ = if AList.defined (op =) the_solvers name
    1.13 +          then warning ("SAT solver " ^ quote name ^ " was defined before")
    1.14 +          else ();
    1.15 +      in solvers := AList.update (op =) (name, new_solver) the_solvers end;
    1.16  
    1.17  (* ------------------------------------------------------------------------- *)
    1.18  (* invoke_solver: returns the solver associated with the given 'name'        *)
     2.1 --- a/src/Pure/General/output.ML	Wed Jan 31 16:05:12 2007 +0100
     2.2 +++ b/src/Pure/General/output.ML	Wed Jan 31 16:05:13 2007 +0100
     2.3 @@ -24,8 +24,6 @@
     2.4    val priority: string -> unit
     2.5    val tracing: string -> unit
     2.6    val warning: string -> unit
     2.7 -  val change_warn: ('b -> 'a -> bool) -> ('a -> 'b -> 'b) -> ('a -> string) -> 'a -> 'b -> 'b
     2.8 -  val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list
     2.9    val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    2.10    val debugging: bool ref
    2.11    val no_warnings: ('a -> 'b) -> 'a -> 'b
    2.12 @@ -155,12 +153,6 @@
    2.13  
    2.14  (* overwriting change with warning *)
    2.15  
    2.16 -fun change_warn ex upd msg x xs =
    2.17 -  (if ex xs x then warning (msg x) else (); upd x xs);
    2.18 -
    2.19 -
    2.20 -(* AList operations *)
    2.21 -
    2.22  fun overwrite (al, p as (key, _)) =
    2.23    let fun over ((q as (keyi, _)) :: pairs) =
    2.24              if keyi = key then p :: pairs else q :: (over pairs)
    2.25 @@ -171,10 +163,6 @@
    2.26   (if is_none (AList.lookup (op =) alist a) then () else warning msg;
    2.27    overwrite args);
    2.28  
    2.29 -fun update_warn eq msg (kv as (key, value)) xs =
    2.30 - (if (not o AList.defined eq xs) key then () else warning msg;
    2.31 -  AList.update eq kv xs);
    2.32 -
    2.33  
    2.34  (* add_mode *)
    2.35