# 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;