hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

--- a/src/HOL/HOL.thy	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/HOL.thy	Sat Jul 13 00:50:49 2013 +0200
@@ -37,8 +37,6 @@
 
 setup {*
   Intuitionistic.method_setup @{binding iprover}
-  #> Quickcheck.setup
-  #> Solve_Direct.setup
   #> Subtyping.setup
   #> Case_Product.setup
 *}

--- a/src/HOL/Metis.thy	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Metis.thy	Sat Jul 13 00:50:49 2013 +0200
@@ -56,6 +56,5 @@
 subsection {* Try0 *}
 
 ML_file "Tools/try0.ML"
-setup {* Try0.setup *}
 
 end

--- a/src/HOL/Nitpick.thy	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Nitpick.thy	Sat Jul 13 00:50:49 2013 +0200
@@ -214,7 +214,6 @@
 ML_file "Tools/Nitpick/nitpick_tests.ML"
 
 setup {*
-  Nitpick_Isar.setup #>
   Nitpick_HOL.register_ersatz_global
     [(@{const_name card}, @{const_name card'}),
      (@{const_name setsum}, @{const_name setsum'}),

--- a/src/HOL/Sledgehammer.thy	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Sledgehammer.thy	Sat Jul 13 00:50:49 2013 +0200
@@ -11,7 +11,6 @@
 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 begin
 
-
 ML_file "Tools/Sledgehammer/async_manager.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
@@ -31,6 +30,4 @@
 ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
 
-setup {* Sledgehammer_Isar.setup *}
-
 end

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -13,7 +13,6 @@
   val nitpickN : string
   val nitpick_paramsN : string
   val default_params : theory -> (string * string) list -> params
-  val setup : theory -> theory
 end;
 
 structure Nitpick_Isar : NITPICK_ISAR =
@@ -399,6 +398,6 @@
 
 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
 
-val setup = Try.register_tool (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -11,7 +11,6 @@
   val provers : string Unsynchronized.ref
   val timeout : int Unsynchronized.ref
   val default_params : Proof.context -> (string * string) list -> params
-  val setup : theory -> theory
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -486,6 +485,6 @@
                      (minimize_command [] i) state
   end
 
-val setup = Try.register_tool (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
 
 end;

--- a/src/HOL/Tools/try0.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/HOL/Tools/try0.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -11,7 +11,6 @@
   val try0 :
     Time.time option -> string list * string list * string list * string list
     -> Proof.state -> bool
-  val setup : theory -> theory
 end;
 
 structure Try0 : TRY0 =
@@ -193,6 +192,6 @@
 fun try_try0 auto =
   do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
 
-val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0))
+val _ = Try.tool_setup (try0N, (30, @{option auto_try0}, try_try0))
 
 end;

--- a/src/Pure/Isar/proof.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -32,6 +32,7 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
+  val pretty_goal_messages: state -> Pretty.T list
   val pretty_state: int -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
@@ -336,6 +337,11 @@
 
 (** pretty_state **)
 
+fun pretty_goal_messages state =
+  (case try find_goal state of
+    SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages)
+  | NONE => []);
+
 fun pretty_facts _ _ NONE = []
   | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
 

--- a/src/Tools/quickcheck.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/Tools/quickcheck.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -10,7 +10,6 @@
   val genuineN: string
   val noneN: string
   val unknownN: string
-  val setup: theory -> theory
   (*configuration*)
   val batch_tester : string Config.T
   val size : int Config.T
@@ -564,7 +563,7 @@
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN);
 
-val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
 
 end;
 

--- a/src/Tools/solve_direct.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/Tools/solve_direct.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -16,7 +16,6 @@
   val unknownN: string
   val max_solutions: int Unsynchronized.ref
   val solve_direct: Proof.state -> bool * (string * Proof.state)
-  val setup: theory -> theory
 end;
 
 structure Solve_Direct: SOLVE_DIRECT =
@@ -115,6 +114,6 @@
 
 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
 
-val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
 
 end;

--- a/src/Tools/try.ML	Sat Jul 13 00:24:05 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 00:50:49 2013 +0200
@@ -13,9 +13,9 @@
 
   val serial_commas : string -> string list -> string list
   val subgoal_count : Proof.state -> int
-  val register_tool : tool -> theory -> theory
   val get_tools : theory -> tool list
   val try_tools : Proof.state -> (string * string) option
+  val tool_setup : tool -> unit
 end;
 
 structure Try : TRY =
@@ -65,6 +65,7 @@
 
 val register_tool = Data.map o Ord_List.insert tool_ord
 
+
 (* try command *)
 
 fun try_tools state =
@@ -89,7 +90,7 @@
     (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
 
-(* automatic try *)
+(* automatic try (TTY) *)
 
 fun auto_try state =
   get_tools (Proof.theory_of state)
@@ -111,4 +112,35 @@
       state
   end))
 
+
+(* asynchronous print function (PIDE) *)
+
+fun print_function ((name, (weight, auto, tool)): tool) =
+  Command.print_function {name = name, pri = ~ weight, persistent = true}
+    (fn {command_name} =>
+      if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
+        SOME (fn _ => fn st =>
+          let
+            val auto_time_limit = Options.default_real @{option auto_time_limit}
+          in
+            if auto_time_limit > 0.0 then
+              (case try Toplevel.proof_of st of
+                SOME state =>
+                  (case
+                    (try o TimeLimit.timeLimit (seconds auto_time_limit))
+                      (fn () => tool true state) () of
+                    SOME (true, (_, state')) =>
+                      Pretty.writeln (Pretty.chunks (Proof.pretty_goal_messages state'))
+                  | _ => ())
+              | NONE => ())
+            else ()
+          end)
+      else NONE);
+
+
+(* hybrid tool setup *)
+
+fun tool_setup tool =
+  (Context.>> (Context.map_theory (register_tool tool)); print_function tool);
+
 end;