--- a/src/HOL/Tools/atp_manager.ML Mon Mar 30 20:49:27 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Mon Mar 30 21:42:12 2009 +0200
@@ -19,7 +19,7 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
+ type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
@@ -133,7 +133,7 @@
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store))
in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
- | NONE =>state));
+ | NONE => state));
(* kill excessive atp threads *)
@@ -168,12 +168,14 @@
fun print_new_messages () =
let val to_print = Synchronized.change_result state
(fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (messages, make_state timeout_heap oldest_heap active cancelling [] store))
- in if null to_print then ()
- else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end;
+ (messages, make_state timeout_heap oldest_heap active cancelling [] store))
+ in
+ if null to_print then ()
+ else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
+ end;
-(* start a watching thread which runs forever -- only one may exist *)
+(* start a watching thread -- only one may exist *)
fun check_thread_manager () = CRITICAL (fn () =>
if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
@@ -203,7 +205,7 @@
in SOME (map #2 timeout_threads, state') end
end
in
- while not(empty_state state) do
+ while not (empty_state state) do
(Synchronized.timed_access state time_limit action
|> these
|> List.app (unregister (false, "Interrupted (reached timeout)"));
@@ -313,7 +315,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
+ val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg
@@ -361,7 +363,7 @@
val _ =
OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
(Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+ Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
end;