# HG changeset patch
# User blanchet
# Date 1284363394 -7200
# Node ID c0bb925ae912de762a7fa9878725269225cd4bd3
# Parent  c277c79fb9db0eeb01bdba972e9ec613abe239b7
no timeout for Auto Try, since the Auto Tools framework takes care of timeouts

diff -r c277c79fb9db -r c0bb925ae912 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Sat Sep 11 16:41:15 2010 +0200
+++ b/src/HOL/Tools/try.ML	Mon Sep 13 09:36:34 2010 +0200
@@ -24,16 +24,17 @@
 
 val timeout = Time.fromSeconds 5
 
-fun can_apply pre post tac st =
+fun can_apply auto pre post tac st =
   let val {goal, ...} = Proof.goal st in
-    case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
+    case (if auto then fn f => fn x => f x
+          else TimeLimit.timeLimit timeout) (Seq.pull o tac) (pre st) of
       SOME (x, _) => nprems_of (post x) < nprems_of goal
     | NONE => false
   end
 
-fun do_generic command pre post apply st =
+fun do_generic auto command pre post apply st =
   let val timer = Timer.startRealTimer () in
-    if can_apply pre post apply st then
+    if can_apply auto pre post apply st then
       SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
     else
       NONE
@@ -47,8 +48,8 @@
     Method.apply (named_method thy name) ctxt []
   end
 
-fun do_named_method name st =
-  do_generic name (#goal o Proof.goal) snd
+fun do_named_method name auto st =
+  do_generic auto name (#goal o Proof.goal) snd
              (apply_named_method name (Proof.context_of st)) st
 
 fun apply_named_method_on_first_goal name ctxt =
@@ -56,8 +57,8 @@
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name st =
-  do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
+fun do_named_method_on_first_goal name auto st =
+  do_generic auto (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,7 +72,7 @@
 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 st)
+  case do_methods |> Par_List.map (fn f => f auto st)
                   |> map_filter I |> sort (int_ord o pairself snd) of
     [] => (if auto then () else writeln "No proof found."; (false, st))
   | xs as (s, _) :: _ =>