initial delay for automatically tried tools;

--- a/src/HOL/Tools/etc/options	Sat Jul 13 18:13:09 2013 +0200
+++ b/src/HOL/Tools/etc/options	Sat Jul 13 18:33:33 2013 +0200
@@ -1,6 +1,9 @@
 (* :mode=isabelle-options: *)
 
-section {* Isabelle/HOL proof tools *}
+section {* Automatically tried tools *}
+
+public option auto_time_start : real = 1.0
+  -- "initial delay for automatically tried tools (seconds)"
 
 public option auto_time_limit : real = 2.0
   -- "time limit for automatically tried tools (seconds > 0)"

--- a/src/Pure/PIDE/command.ML	Sat Jul 13 18:13:09 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Jul 13 18:33:33 2013 +0200
@@ -16,7 +16,8 @@
   val print: bool -> string -> eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print_function: string ->
-    ({command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option) -> unit
+    ({command_name: string} ->
+      {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
@@ -192,13 +193,14 @@
 (* print *)
 
 datatype print = Print of
- {name: string, pri: int, persistent: bool,
+ {name: string, delay: Time.time, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option;
+  {command_name: string} ->
+    {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
 
 local
 
@@ -224,7 +226,7 @@
   let
     fun new_print (name, get_pr) =
       let
-        fun make_print strict {pri, persistent, print_fn} =
+        fun make_print strict {delay, pri, persistent, print_fn} =
           let
             val exec_id = Document_ID.make ();
             fun process () =
@@ -237,7 +239,7 @@
               end;
           in
            Print {
-             name = name, pri = pri, persistent = persistent,
+             name = name, delay = delay, pri = pri, persistent = persistent,
              exec_id = exec_id, print_process = memo exec_id process}
           end;
       in
@@ -246,7 +248,8 @@
         | Exn.Res (SOME pr) => SOME (make_print false pr)
         | Exn.Exn exn =>
             SOME (make_print true
-              {pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
+              {delay = Time.zeroTime, pri = 0, persistent = false,
+                print_fn = fn _ => fn _ => reraise exn}))
       end;
 
     val new_prints =
@@ -273,14 +276,16 @@
 
 val _ =
   print_function "print_state"
-    (fn {command_name} => SOME {pri = 0, persistent = true, print_fn = fn tr => fn st' =>
-      let
-        val is_init = Keyword.is_theory_begin command_name;
-        val is_proof = Keyword.is_proof command_name;
-        val do_print =
-          not is_init andalso
-            (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-      in if do_print then Toplevel.print_state false st' else () end});
+    (fn {command_name} =>
+      SOME {delay = Time.zeroTime, pri = 0, persistent = true,
+        print_fn = fn tr => fn st' =>
+          let
+            val is_init = Keyword.is_theory_begin command_name;
+            val is_proof = Keyword.is_proof command_name;
+            val do_print =
+              not is_init andalso
+                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+          in if do_print then Toplevel.print_state false st' else () end});
 
 
 (* combined execution *)
@@ -295,10 +300,18 @@
 
 local
 
-fun run_print execution_id (Print {name, pri, print_process, ...}) =
-  (if Multithreading.enabled () then
-    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
-  else memo_exec) execution_id print_process;
+fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
+  if Multithreading.enabled () then
+    let
+      val group = Future.worker_subgroup ();
+      fun fork () =
+        memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
+          execution_id print_process;
+    in
+      if delay = Time.zeroTime then fork ()
+      else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
+    end
+  else memo_exec execution_id print_process;
 
 in
 

--- a/src/Tools/try.ML	Sat Jul 13 18:13:09 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 18:33:33 2013 +0200
@@ -119,18 +119,22 @@
   Command.print_function name
     (fn {command_name} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
-        SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
-          let
-            val state = Toplevel.proof_of st
-            val auto_time_limit = Options.default_real @{option auto_time_limit}
-          in
-            if auto_time_limit > 0.0 then
-              (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
-                (true, (_, state')) =>
-                  List.app Pretty.writeln (Proof.pretty_goal_messages state')
-              | _ => ())
-            else ()
-          end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
+        SOME
+         {delay = seconds (Options.default_real @{option auto_time_start}),
+          pri = ~ weight,
+          persistent = true,
+          print_fn = fn _ => fn st =>
+            let
+              val state = Toplevel.proof_of st
+              val auto_time_limit = Options.default_real @{option auto_time_limit}
+            in
+              if auto_time_limit > 0.0 then
+                (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
+                  (true, (_, state')) =>
+                    List.app Pretty.writeln (Proof.pretty_goal_messages state')
+                | _ => ())
+              else ()
+            end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
       else NONE)