# HG changeset patch # User wenzelm # Date 1238442132 -7200 # Node ID 95cbadcd47fcdd90770d7e3ebd7db823df566a7f # Parent 09306de1d99d06f6802a0d6fc2eabe9c6491272d tuned spacing and formatting; diff -r 09306de1d99d -r 95cbadcd47fc src/HOL/Tools/atp_manager.ML --- 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;