early warning when Sledgehammer finds a proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -109,7 +109,7 @@
 
 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
       expect, ...}) mode writeln_result only learn
-    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
+    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name =
   let
     val ctxt = Proof.context_of state
 
@@ -124,7 +124,8 @@
        factss = factss
        |> map (apsnd ((not (is_ho_atp ctxt name)
            ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false))
-         #> take num_facts))}
+         #> take num_facts)),
+       found_proof = found_proof}
 
     fun print_used_facts used_facts used_from =
       tag_list 1 used_from
@@ -244,8 +245,18 @@
     | n =>
       let
         val _ = Proof.assert_backward state
-        val print =
-          if mode = Normal andalso is_none writeln_result then writeln else K ()
+        val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
+
+        val found_proof =
+          if mode = Normal then
+            let val proof_found = Synchronized.var "proof_found" false in
+              fn () =>
+                if Synchronized.change_result proof_found (rpair true) then ()
+                else (writeln_result |> the_default writeln) "Proof found..."
+            end
+          else
+            I
+
         val ctxt = Proof.context_of state
         val keywords = Thy_Header.get_keywords' ctxt
         val {facts = chained, goal, ...} = Proof.goal state
@@ -288,7 +299,7 @@
             val factss = get_factss provers
             val problem =
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-               factss = factss}
+               factss = factss, found_proof = found_proof}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
             val launch = launch_prover params mode writeln_result only learn
           in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -834,7 +834,7 @@
   let
     val problem =
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
-       subgoal_count = 1, factss = [("", facts)]}
+       subgoal_count = 1, factss = [("", facts)], found_proof = I}
   in
     get_minimizing_prover ctxt MaSh (K ()) prover params problem
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -49,7 +49,8 @@
      goal : thm,
      subgoal : int,
      subgoal_count : int,
-     factss : (string * fact list) list}
+     factss : (string * fact list) list,
+     found_proof : unit -> unit}
 
   type prover_result =
     {outcome : atp_failure option,
@@ -133,7 +134,8 @@
    goal : thm,
    subgoal : int,
    subgoal_count : int,
-   factss : (string * fact list) list}
+   factss : (string * fact list) list,
+   found_proof : unit -> unit}
 
 type prover_result =
   {outcome : atp_failure option,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -133,7 +133,7 @@
     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
      slice, minimize, timeout, preplay_timeout, ...} : params)
-    ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+    ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -318,7 +318,7 @@
                   in
                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
                   end
-                | NONE => NONE)
+                | NONE => (found_proof (); NONE))
               | _ => outcome)
           in
             ((SOME key, value), (output, run_time, facts, atp_proof, outcome),

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -98,7 +98,7 @@
        expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)]}
+       factss = [("", facts)], found_proof = I}
     val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
         message} =
       prover params problem

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -180,7 +180,7 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, ...})
-    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+    ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -199,6 +199,7 @@
       (case outcome of
         NONE =>
         let
+          val _ = found_proof ();
           val smt_method = smt_proofs <> SOME false
           val preferred_methss =
             (if smt_method then SMT_Method else Metis_Method (NONE, NONE),