src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 33312 6ca8a7984fd9
parent 33292 affe60b3d864
child 33316 6a72af4e84b8
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:08:45 2009 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:09:16 2009 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  (* unregister ATP thread *)
     1.6  
     1.7 -fun unregister (success, message) thread = Synchronized.change global_state
     1.8 +fun unregister message thread = Synchronized.change global_state
     1.9    (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
    1.10      (case lookup_thread active thread of
    1.11        SOME (birth_time, _, description) =>
    1.12 @@ -149,7 +149,7 @@
    1.13          do
    1.14            (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
    1.15              |> these
    1.16 -            |> List.app (unregister (false, "Interrupted (reached timeout)"));
    1.17 +            |> List.app (unregister "Interrupted (reached timeout)");
    1.18              print_new_messages ();
    1.19              (*give threads some time to respond to interrupt*)
    1.20              OS.Process.sleep min_wait_time)
    1.21 @@ -263,14 +263,11 @@
    1.22            let
    1.23              val _ = register birth_time death_time (Thread.self (), desc);
    1.24              val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
    1.25 -            val result =
    1.26 -              let val {success, message, ...} = prover (! timeout) problem;
    1.27 -              in (success, message) end
    1.28 +            val message = #message (prover (! timeout) problem)
    1.29                handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
    1.30 -                  (true, "Empty clause: Try this command: " ^
    1.31 -                    Markup.markup Markup.sendback "apply metis")
    1.32 -                | ERROR msg => (false, "Error: " ^ msg);
    1.33 -            val _ = unregister result (Thread.self ());
    1.34 +                  "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    1.35 +                | ERROR msg => ("Error: " ^ msg);
    1.36 +            val _ = unregister message (Thread.self ());
    1.37            in () end)
    1.38        in () end);
    1.39