# HG changeset patch
# User blanchet
# Date 1376386496 -7200
# Node ID ea02bc4e9a5f3ffdd6a9e9018c8661a7725c9f27
# Parent  9a47c82560549c6a3b56755f5878732e644333df
added flag for jEdit/PIDE asynchronous mode

diff -r 9a47c8256054 -r ea02bc4e9a5f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 13 11:34:56 2013 +0200
@@ -16,7 +16,7 @@
   type play = Sledgehammer_Reconstructor.play
   type minimize_command = Sledgehammer_Reconstructor.minimize_command
 
-  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+  datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
 
   type params =
     {debug : bool,
@@ -161,7 +161,7 @@
 
 (** The Sledgehammer **)
 
-datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
@@ -667,6 +667,7 @@
 fun suffix_of_mode Auto_Try = "_try"
   | suffix_of_mode Try = "_try"
   | suffix_of_mode Normal = ""
+  | suffix_of_mode Normal_Result = ""
   | suffix_of_mode MaSh = ""
   | suffix_of_mode Auto_Minimize = "_min"
   | suffix_of_mode Minimize = "_min"
@@ -930,7 +931,7 @@
          (output, run_time, used_from, atp_proof, outcome)) =
       with_cleanup clean_up run () |> tap export
     val important_message =
-      if mode = Normal andalso
+      if (mode = Normal orelse mode = Normal_Result) andalso
          random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
         extract_important_message output
       else
diff -r 9a47c8256054 -r ea02bc4e9a5f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 13 11:34:56 2013 +0200
@@ -157,7 +157,7 @@
             state |> Proof.map_context
               (Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
           else
-            ((if outcome_code = someN orelse mode = Normal then
+            ((if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
                quote name ^ ": " ^ message ()
              else
                "")
@@ -294,7 +294,7 @@
         |> Par_List.map (fn f => ignore (f (unknownN, state)))
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
       fun maybe f (accum as (outcome_code, _)) =
-        accum |> (mode = Normal orelse outcome_code <> someN) ? f
+        accum |> (mode = Normal orelse mode = Normal_Result orelse outcome_code <> someN) ? f
     in
       (unknownN, state)
       |> (if blocking then