--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Oct 02 21:15:25 2015 +0200
@@ -10,13 +10,9 @@
signature ASYNC_MANAGER_LEGACY =
sig
- val break_into_chunks : string -> string list
val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) ->
unit
- val kill_threads : string -> string -> unit
val has_running_threads : string -> bool
- val running_threads : string -> string -> unit
- val thread_messages : string -> string -> int option -> unit
end;
structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY =
@@ -31,9 +27,6 @@
Simple_Thread.attributes
{name = "async_manager", stack_limit = NONE, interrupts = interrupts});
-val message_store_limit = 20
-val message_display_limit = 10
-
fun implode_message (workers, work) =
space_implode " " (Try.serial_commas "and" workers) ^ work
@@ -54,18 +47,17 @@
(Thread.thread
* (string * Time.time * Time.time * (string * string))) list,
canceling: (Thread.thread * (string * Time.time * (string * string))) list,
- messages: (bool * (string * (string * string))) list,
- store: (string * (string * string)) list}
+ messages: (bool * (string * (string * string))) list}
-fun make_state manager timeout_heap active canceling messages store : state =
- {manager = manager, timeout_heap = timeout_heap, active = active,
- canceling = canceling, messages = messages, store = store}
+fun make_state manager timeout_heap active canceling messages : state =
+ {manager = manager, timeout_heap = timeout_heap, active = active, canceling = canceling,
+ messages = messages}
-val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [] [])
+val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [])
fun unregister (urgent, message) thread =
Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ (fn state as {manager, timeout_heap, active, canceling, messages} =>
(case lookup_thread active thread of
SOME (tool, _, _, desc as (worker, its_desc)) =>
let
@@ -75,50 +67,30 @@
val message' =
(worker, its_desc ^ (if message = "" then "" else "\n" ^ message))
val messages' = (urgent, (tool, message')) :: messages
- val store' = (tool, message') ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store))
- in make_state manager timeout_heap active' canceling' messages' store' end
+ in make_state manager timeout_heap active' canceling' messages' end
| NONE => state))
val min_wait_time = seconds 0.3
val max_wait_time = seconds 10.0
-fun replace_all bef aft =
- let
- fun aux seen "" = String.implode (rev seen)
- | aux seen s =
- if String.isPrefix bef s then
- aux seen "" ^ aft ^ aux [] (unprefix bef s)
- else
- aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
- in aux [] end
-
-(* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in
- "proof" is not highlighted. *)
-val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000"
-
fun print_new_messages () =
Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (fn {manager, timeout_heap, active, canceling, messages} =>
messages
|> List.partition
(fn (urgent, _) =>
(null active andalso null canceling) orelse urgent)
- ||> (fn postponed_messages =>
- make_state manager timeout_heap active canceling
- postponed_messages store))
+ ||> make_state manager timeout_heap active canceling)
|> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
|> AList.group (op =)
|> List.app (fn ((_, ""), _) => ()
| ((tool, work), workers) =>
tool ^ ": " ^
implode_message (workers |> sort_distinct string_ord, work)
- |> break_into_chunks
- |> List.app writeln)
+ |> writeln)
fun check_thread_manager () = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ (fn state as {manager, timeout_heap, active, canceling, messages} =>
if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
else let val manager = SOME (make_thread false (fn () =>
let
@@ -128,7 +100,7 @@
| SOME (time, _) => time)
(*action: find threads whose timeout is reached, and interrupt canceling threads*)
- fun action {manager, timeout_heap, active, canceling, messages, store} =
+ fun action {manager, timeout_heap, active, canceling, messages} =
let val (timeout_threads, timeout_heap') =
Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
in
@@ -138,14 +110,14 @@
let
val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
val canceling' = filter (Thread.isActive o #1) canceling
- val state' = make_state manager timeout_heap' active canceling' messages store
+ val state' = make_state manager timeout_heap' active canceling' messages
in SOME (map #2 timeout_threads, state') end
end
in
while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
+ (fn state as {timeout_heap, active, canceling, messages, ...} =>
if null active andalso null canceling andalso null messages
- then (false, make_state NONE timeout_heap active canceling messages store)
+ then (false, make_state NONE timeout_heap active canceling messages)
else (true, state))
do
(Synchronized.timed_access global_state
@@ -156,15 +128,15 @@
(* give threads some time to respond to interrupt *)
OS.Process.sleep min_wait_time)
end))
- in make_state manager timeout_heap active canceling messages store end)
+ in make_state manager timeout_heap active canceling messages end)
fun register tool birth_time death_time desc thread =
(Synchronized.change global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (fn {manager, timeout_heap, active, canceling, messages} =>
let
val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap
val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active
- val state' = make_state manager timeout_heap' active' canceling messages store
+ val state' = make_state manager timeout_heap' active' canceling messages
in state' end);
check_thread_manager ())
@@ -177,60 +149,7 @@
in unregister (f ()) self end);
())
-fun kill_threads tool das_wort_worker = Synchronized.change global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- let
- val killing =
- map_filter (fn (th, (tool', _, _, desc)) =>
- if tool' = tool then SOME (th, (tool', Time.now (), desc))
- else NONE) active
- val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
- val _ =
- if null killing then ()
- else writeln ("Interrupted active " ^ das_wort_worker ^ "s.")
- in state' end)
-
-fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
-
fun has_running_threads tool =
exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state))
-fun running_threads tool das_wort_worker =
- let
- val {active, canceling, ...} = Synchronized.value global_state
- val now = Time.now ()
- fun running_info (_, (tool', birth_time, death_time, desc)) =
- if tool' = tool then
- SOME ("Running: " ^ str_of_time (Time.- (now, birth_time)) ^ " -- " ^
- str_of_time (Time.- (death_time, now)) ^ " to live:\n" ^ op ^ desc)
- else
- NONE
- fun canceling_info (_, (tool', death_time, desc)) =
- if tool' = tool then
- SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
- str_of_time (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc)
- else
- NONE
- val running =
- case map_filter running_info active of
- [] => ["No " ^ das_wort_worker ^ "s running."]
- | ss => "Running " ^ das_wort_worker ^ "s" :: ss
- val interrupting =
- case map_filter canceling_info canceling of
- [] => []
- | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
- in writeln (space_implode "\n\n" (running @ interrupting)) end
-
-fun thread_messages tool das_wort_worker opt_limit =
- let
- val limit = the_default message_display_limit opt_limit
- val tool_store = Synchronized.value global_state
- |> #store |> filter (curry (op =) tool o fst)
- val header =
- "Recent " ^ das_wort_worker ^ " messages" ^
- (if length tool_store <= limit then ":"
- else " (" ^ string_of_int limit ^ " displayed):")
- val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
- in List.app writeln (header :: maps break_into_chunks ss) end
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Oct 02 21:15:25 2015 +0200
@@ -76,7 +76,7 @@
fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) =
let
fun process_steps [] = []
- | process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1),
+ | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1),
Prove ([Show], [], l2, t2, _, _, _, comment2)]) =
if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)]
else steps