equal
deleted
inserted
replaced
89 case try (tool true) state of |
89 case try (tool true) state of |
90 SOME (true, (_, state)) => SOME state |
90 SOME (true, (_, state)) => SOME state |
91 | _ => NONE) |
91 | _ => NONE) |
92 |> the_default state |
92 |> the_default state |
93 |
93 |
94 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => |
|
95 let |
|
96 val auto_time_limit = Options.default_real @{system_option auto_time_limit} |
|
97 in |
|
98 if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then |
|
99 TimeLimit.timeLimit (seconds auto_time_limit) auto_try state |
|
100 handle TimeLimit.TimeOut => state |
|
101 else |
|
102 state |
|
103 end)) |
|
104 |
|
105 |
94 |
106 (* asynchronous print function (PIDE) *) |
95 (* asynchronous print function (PIDE) *) |
107 |
96 |
108 fun print_function ((name, (weight, auto, tool)): tool) = |
97 fun print_function ((name, (weight, auto, tool)): tool) = |
109 Command.print_function ("auto_" ^ name) |
98 Command.print_function ("auto_" ^ name) |