# HG changeset patch
# User blanchet
# Date 1291843072 -3600
# Node ID 2e69fb6331cbba51cc18f9e7b015537e1b30ecaa
# Parent  54eb8e7c7f9bd874aa2b370a2bfbece236fa7fcb
moved function to later module

diff -r 54eb8e7c7f9b -r 2e69fb6331cb src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -48,6 +48,7 @@
 
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
+  val das_Tool : string
   val is_smt_prover : Proof.context -> string -> bool
   val is_prover_available : Proof.context -> string -> bool
   val is_prover_installed : Proof.context -> string -> bool
@@ -65,9 +66,6 @@
   val running_provers : unit -> unit
   val messages : int option -> unit
   val get_prover : Proof.context -> bool -> string -> prover
-  val run_prover :
-    params -> bool -> (string -> minimize_command) -> bool -> prover_problem
-    -> string -> bool * Proof.state
   val setup : theory -> theory
 end;
 
@@ -249,19 +247,6 @@
   |> Exn.release
   |> tap (after path)
 
-fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
-                       n goal =
-  quote name ^
-  (if verbose then
-     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
-   else
-     "") ^
-  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
-  (if blocking then
-     ""
-   else
-     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
-
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
@@ -580,66 +565,6 @@
       error ("No such prover: " ^ name ^ ".")
   end
 
-fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
-               auto minimize_command only
-               {state, goal, subgoal, subgoal_count, facts} name =
-  let
-    val ctxt = Proof.context_of state
-    val birth_time = Time.now ()
-    val death_time = Time.+ (birth_time, timeout)
-    val max_relevant =
-      the_default (default_max_relevant_for_prover ctxt name) max_relevant
-    val num_facts = length facts |> not only ? Integer.min max_relevant
-    val desc =
-      prover_description ctxt params name num_facts subgoal subgoal_count goal
-    val prover = get_prover ctxt auto name
-    val problem =
-      {state = state, goal = goal, subgoal = subgoal,
-       subgoal_count = subgoal_count, facts = take num_facts facts}
-    fun go () =
-      let
-        fun really_go () =
-          prover params (minimize_command name) problem
-          |> (fn {outcome, message, ...} =>
-                 (if is_some outcome then "none" else "some", message))
-        val (outcome_code, message) =
-          if debug then
-            really_go ()
-          else
-            (really_go ()
-             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
-                  | exn =>
-                    if Exn.is_interrupt exn then
-                      reraise exn
-                    else
-                      ("unknown", "Internal error:\n" ^
-                                  ML_Compiler.exn_message exn ^ "\n"))
-        val _ =
-          if expect = "" orelse outcome_code = expect then
-            ()
-          else if blocking then
-            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
-          else
-            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
-      in (outcome_code = "some", message) end
-  in
-    if auto then
-      let val (success, message) = TimeLimit.timeLimit timeout go () in
-        (success, state |> success ? Proof.goal_message (fn () =>
-             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
-                 (Pretty.str message)]))
-      end
-    else if blocking then
-      let val (success, message) = TimeLimit.timeLimit timeout go () in
-        List.app Output.urgent_message
-                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
-        (success, state)
-      end
-    else
-      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
-       (false, state))
-  end
-
 val setup =
   dest_dir_setup
   #> problem_prefix_setup
diff -r 54eb8e7c7f9b -r 2e69fb6331cb src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
@@ -25,6 +25,79 @@
 open Sledgehammer_ATP_Translate
 open Sledgehammer_Provers
 
+fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
+                       n goal =
+  quote name ^
+  (if verbose then
+     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
+   else
+     "") ^
+  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+  (if blocking then
+     ""
+   else
+     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+
+fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
+               auto minimize_command only
+               {state, goal, subgoal, subgoal_count, facts} name =
+  let
+    val ctxt = Proof.context_of state
+    val birth_time = Time.now ()
+    val death_time = Time.+ (birth_time, timeout)
+    val max_relevant =
+      the_default (default_max_relevant_for_prover ctxt name) max_relevant
+    val num_facts = length facts |> not only ? Integer.min max_relevant
+    val desc =
+      prover_description ctxt params name num_facts subgoal subgoal_count goal
+    val prover = get_prover ctxt auto name
+    val problem =
+      {state = state, goal = goal, subgoal = subgoal,
+       subgoal_count = subgoal_count, facts = take num_facts facts}
+    fun go () =
+      let
+        fun really_go () =
+          prover params (minimize_command name) problem
+          |> (fn {outcome, message, ...} =>
+                 (if is_some outcome then "none" else "some", message))
+        val (outcome_code, message) =
+          if debug then
+            really_go ()
+          else
+            (really_go ()
+             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
+                  | exn =>
+                    if Exn.is_interrupt exn then
+                      reraise exn
+                    else
+                      ("unknown", "Internal error:\n" ^
+                                  ML_Compiler.exn_message exn ^ "\n"))
+        val _ =
+          if expect = "" orelse outcome_code = expect then
+            ()
+          else if blocking then
+            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+          else
+            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
+      in (outcome_code = "some", message) end
+  in
+    if auto then
+      let val (success, message) = TimeLimit.timeLimit timeout go () in
+        (success, state |> success ? Proof.goal_message (fn () =>
+             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
+                 (Pretty.str message)]))
+      end
+    else if blocking then
+      let val (success, message) = TimeLimit.timeLimit timeout go () in
+        List.app Output.urgent_message
+                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
+        (success, state)
+      end
+    else
+      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
+       (false, state))
+  end
+
 (* FUDGE *)
 val auto_max_relevant_divisor = 2