equal
deleted
inserted
replaced
39 open Sledgehammer_Proof_Methods |
39 open Sledgehammer_Proof_Methods |
40 open Sledgehammer_Isar_Proof |
40 open Sledgehammer_Isar_Proof |
41 |
41 |
42 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
42 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
43 |
43 |
44 fun par_list_map_filter_with_timeout get_time timeout0 f xs = |
44 fun par_list_map_filter_with_timeout _ _ _ [] = [] |
45 let |
45 | par_list_map_filter_with_timeout get_time timeout0 f xs = |
46 val next_timeout = Unsynchronized.ref timeout0 |
46 let |
47 |
47 val next_timeout = Unsynchronized.ref timeout0 |
48 fun apply_f x = |
48 |
49 let val timeout = !next_timeout in |
49 fun apply_f x = |
50 if timeout = Time.zeroTime then |
50 let val timeout = !next_timeout in |
51 NONE |
51 if timeout = Time.zeroTime then |
52 else |
52 NONE |
53 let val y = f timeout x in |
53 else |
54 (case get_time y of |
54 let val y = f timeout x in |
55 SOME time => next_timeout := time |
55 (case get_time y of |
56 | _ => ()); |
56 SOME time => next_timeout := time |
57 SOME y |
57 | _ => ()); |
58 end |
58 SOME y |
59 end |
59 end |
60 in |
60 end |
61 map_filter I (Par_List.map apply_f xs) |
61 in |
62 end |
62 map_filter I (Par_List.map apply_f xs) |
|
63 end |
63 |
64 |
64 fun enrich_context_with_local_facts proof ctxt = |
65 fun enrich_context_with_local_facts proof ctxt = |
65 let |
66 let |
66 val thy = Proof_Context.theory_of ctxt |
67 val thy = Proof_Context.theory_of ctxt |
67 |
68 |