src/HOL/Tools/try.ML

 *)
 
 signature TRY =
 sig
   val auto : bool Unsynchronized.ref
-  val invoke_try : Proof.state -> unit
+  val invoke_try : Time.time option -> Proof.state -> bool
   val setup : theory -> theory
 end;
 
 structure Try : TRY =
 struct

   ProofGeneralPgip.add_preference Preferences.category_tracing
   (setmp_noncritical auto true (fn () =>
     Preferences.bool_pref auto
       "auto-try" "Try standard proof methods.") ());
 
-val timeout = Time.fromSeconds 5
+val default_timeout = Time.fromSeconds 5
 
-fun can_apply auto pre post tac st =
+fun can_apply timeout_opt pre post tac st =
   let val {goal, ...} = Proof.goal st in
-    case (if auto then fn f => fn x => f x
-          else TimeLimit.timeLimit timeout) (Seq.pull o tac) (pre st) of
+    case (case timeout_opt of
+            SOME timeout => TimeLimit.timeLimit timeout
+          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
       SOME (x, _) => nprems_of (post x) < nprems_of goal
     | NONE => false
   end
 
-fun do_generic auto command pre post apply st =
+fun do_generic timeout_opt command pre post apply st =
   let val timer = Timer.startRealTimer () in
-    if can_apply auto pre post apply st then
+    if can_apply timeout_opt pre post apply st then
       SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
     else
       NONE
   end
 

 fun apply_named_method name ctxt =
   let val thy = ProofContext.theory_of ctxt in
     Method.apply (named_method thy name) ctxt []
   end
 
-fun do_named_method name auto st =
-  do_generic auto name (#goal o Proof.goal) snd
+fun do_named_method name timeout_opt st =
+  do_generic timeout_opt name (#goal o Proof.goal) snd
              (apply_named_method name (Proof.context_of st)) st
 
 fun apply_named_method_on_first_goal name ctxt =
   let val thy = ProofContext.theory_of ctxt in
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name auto st =
-  do_generic auto (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
+fun do_named_method_on_first_goal name timeout_opt st =
+  do_generic timeout_opt
+             (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
                       else "")) I (#goal o Proof.goal)
              (apply_named_method_on_first_goal name (Proof.context_of st)) st
 
 val all_goals_named_methods = ["auto"]
 val first_goal_named_methods =

   map do_named_method_on_first_goal all_goals_named_methods @
   map do_named_method first_goal_named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
 
-fun do_try auto st =
-  case do_methods |> Par_List.map (fn f => f auto st)
+fun do_try auto timeout_opt st =
+  case do_methods |> Par_List.map (fn f => f timeout_opt st)
                   |> map_filter I |> sort (int_ord o pairself snd) of
     [] => (if auto then () else writeln "No proof found."; (false, st))
   | xs as (s, _) :: _ =>
     let
       val xs = xs |> map swap |> AList.coalesce (op =)

                                                   [Pretty.str message]])
                     else
                       tap (fn _ => priority message)))
     end
 
-val invoke_try = do_try false #> K ()
+val invoke_try = fst oo do_try false
 
 val tryN = "try"
 
 val _ =
   Outer_Syntax.improper_command tryN
       "try a combination of proof methods" Keyword.diag
-      (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
+      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
+                                    o Toplevel.proof_of)))
 
-fun auto_try st = if not (!auto) then (false, st) else do_try true st
+fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
 
 val setup = Auto_Tools.register_tool (tryN, auto_try)
 
 end;