# HG changeset patch
# User blanchet
# Date 1284380905 -7200
# Node ID 1899349a5026402ec366cc4b4bf716f50d51acb5
# Parent  87a9ff4d5817f8c8fcc6258e3c6c8035f813f3c1
change signature of "Try.invoke_try" to make it more flexible

diff -r 87a9ff4d5817 -r 1899349a5026 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Mon Sep 13 13:12:33 2010 +0200
+++ b/src/HOL/Tools/try.ML	Mon Sep 13 14:28:25 2010 +0200
@@ -7,7 +7,7 @@
 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;
 
@@ -22,19 +22,20 @@
     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
@@ -48,8 +49,8 @@
     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 =
@@ -57,8 +58,9 @@
     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
 
@@ -71,8 +73,8 @@
 
 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, _) :: _ =>
@@ -95,16 +97,17 @@
                       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)