1.1 --- a/src/HOL/Tools/etc/options Sat Jul 13 18:13:09 2013 +0200
1.2 +++ b/src/HOL/Tools/etc/options Sat Jul 13 18:33:33 2013 +0200
1.3 @@ -1,6 +1,9 @@
1.4 (* :mode=isabelle-options: *)
1.5
1.6 -section {* Isabelle/HOL proof tools *}
1.7 +section {* Automatically tried tools *}
1.8 +
1.9 +public option auto_time_start : real = 1.0
1.10 + -- "initial delay for automatically tried tools (seconds)"
1.11
1.12 public option auto_time_limit : real = 2.0
1.13 -- "time limit for automatically tried tools (seconds > 0)"
2.1 --- a/src/Pure/PIDE/command.ML Sat Jul 13 18:13:09 2013 +0200
2.2 +++ b/src/Pure/PIDE/command.ML Sat Jul 13 18:33:33 2013 +0200
2.3 @@ -16,7 +16,8 @@
2.4 val print: bool -> string -> eval -> print list -> print list option
2.5 type print_fn = Toplevel.transition -> Toplevel.state -> unit
2.6 val print_function: string ->
2.7 - ({command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option) -> unit
2.8 + ({command_name: string} ->
2.9 + {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
2.10 val no_print_function: string -> unit
2.11 type exec = eval * print list
2.12 val no_exec: exec
2.13 @@ -192,13 +193,14 @@
2.14 (* print *)
2.15
2.16 datatype print = Print of
2.17 - {name: string, pri: int, persistent: bool,
2.18 + {name: string, delay: Time.time, pri: int, persistent: bool,
2.19 exec_id: Document_ID.exec, print_process: unit memo};
2.20
2.21 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
2.22
2.23 type print_function =
2.24 - {command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option;
2.25 + {command_name: string} ->
2.26 + {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
2.27
2.28 local
2.29
2.30 @@ -224,7 +226,7 @@
2.31 let
2.32 fun new_print (name, get_pr) =
2.33 let
2.34 - fun make_print strict {pri, persistent, print_fn} =
2.35 + fun make_print strict {delay, pri, persistent, print_fn} =
2.36 let
2.37 val exec_id = Document_ID.make ();
2.38 fun process () =
2.39 @@ -237,7 +239,7 @@
2.40 end;
2.41 in
2.42 Print {
2.43 - name = name, pri = pri, persistent = persistent,
2.44 + name = name, delay = delay, pri = pri, persistent = persistent,
2.45 exec_id = exec_id, print_process = memo exec_id process}
2.46 end;
2.47 in
2.48 @@ -246,7 +248,8 @@
2.49 | Exn.Res (SOME pr) => SOME (make_print false pr)
2.50 | Exn.Exn exn =>
2.51 SOME (make_print true
2.52 - {pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
2.53 + {delay = Time.zeroTime, pri = 0, persistent = false,
2.54 + print_fn = fn _ => fn _ => reraise exn}))
2.55 end;
2.56
2.57 val new_prints =
2.58 @@ -273,14 +276,16 @@
2.59
2.60 val _ =
2.61 print_function "print_state"
2.62 - (fn {command_name} => SOME {pri = 0, persistent = true, print_fn = fn tr => fn st' =>
2.63 - let
2.64 - val is_init = Keyword.is_theory_begin command_name;
2.65 - val is_proof = Keyword.is_proof command_name;
2.66 - val do_print =
2.67 - not is_init andalso
2.68 - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
2.69 - in if do_print then Toplevel.print_state false st' else () end});
2.70 + (fn {command_name} =>
2.71 + SOME {delay = Time.zeroTime, pri = 0, persistent = true,
2.72 + print_fn = fn tr => fn st' =>
2.73 + let
2.74 + val is_init = Keyword.is_theory_begin command_name;
2.75 + val is_proof = Keyword.is_proof command_name;
2.76 + val do_print =
2.77 + not is_init andalso
2.78 + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
2.79 + in if do_print then Toplevel.print_state false st' else () end});
2.80
2.81
2.82 (* combined execution *)
2.83 @@ -295,10 +300,18 @@
2.84
2.85 local
2.86
2.87 -fun run_print execution_id (Print {name, pri, print_process, ...}) =
2.88 - (if Multithreading.enabled () then
2.89 - memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
2.90 - else memo_exec) execution_id print_process;
2.91 +fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
2.92 + if Multithreading.enabled () then
2.93 + let
2.94 + val group = Future.worker_subgroup ();
2.95 + fun fork () =
2.96 + memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
2.97 + execution_id print_process;
2.98 + in
2.99 + if delay = Time.zeroTime then fork ()
2.100 + else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
2.101 + end
2.102 + else memo_exec execution_id print_process;
2.103
2.104 in
2.105
3.1 --- a/src/Tools/try.ML Sat Jul 13 18:13:09 2013 +0200
3.2 +++ b/src/Tools/try.ML Sat Jul 13 18:33:33 2013 +0200
3.3 @@ -119,18 +119,22 @@
3.4 Command.print_function name
3.5 (fn {command_name} =>
3.6 if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
3.7 - SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
3.8 - let
3.9 - val state = Toplevel.proof_of st
3.10 - val auto_time_limit = Options.default_real @{option auto_time_limit}
3.11 - in
3.12 - if auto_time_limit > 0.0 then
3.13 - (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
3.14 - (true, (_, state')) =>
3.15 - List.app Pretty.writeln (Proof.pretty_goal_messages state')
3.16 - | _ => ())
3.17 - else ()
3.18 - end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
3.19 + SOME
3.20 + {delay = seconds (Options.default_real @{option auto_time_start}),
3.21 + pri = ~ weight,
3.22 + persistent = true,
3.23 + print_fn = fn _ => fn st =>
3.24 + let
3.25 + val state = Toplevel.proof_of st
3.26 + val auto_time_limit = Options.default_real @{option auto_time_limit}
3.27 + in
3.28 + if auto_time_limit > 0.0 then
3.29 + (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
3.30 + (true, (_, state')) =>
3.31 + List.app Pretty.writeln (Proof.pretty_goal_messages state')
3.32 + | _ => ())
3.33 + else ()
3.34 + end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
3.35 else NONE)
3.36
3.37