initial delay for automatically tried tools;
authorwenzelm
Sat Jul 13 18:33:33 2013 +0200 (2013-07-13 ago)
changeset 526515adb5c69af97
parent 52650 4cf6fbf1d9a1
child 52652 ebdbd5c79a13
initial delay for automatically tried tools;
src/HOL/Tools/etc/options
src/Pure/PIDE/command.ML
src/Tools/try.ML
     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