further reduced dependency on legacy async thread manager

--- 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.ML	Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 02 21:15:25 2015 +0200
@@ -60,10 +60,6 @@
     ordered_outcome_codes
   |> the_default unknownN
 
-fun prover_description verbose name num_facts =
-  (quote name,
-   if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
-
 fun is_metis_method (Metis_Method _) = true
   | is_metis_method _ = false
 
@@ -125,8 +121,6 @@
 
     val hard_timeout = time_mult 3.0 timeout
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
-    val birth_time = Time.now ()
-    val death_time = Time.+ (birth_time, hard_timeout)
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts
 
@@ -228,12 +222,8 @@
         val outcome =
           if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
         val _ =
-          if outcome <> "" andalso is_some writeln_result then
-            the writeln_result outcome
-          else
-            outcome
-            |> Async_Manager_Legacy.break_into_chunks
-            |> List.app writeln
+          if outcome <> "" andalso is_some writeln_result then the writeln_result outcome
+          else writeln outcome
       in (outcome_code, []) end
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 02 21:15:25 2015 +0200
@@ -33,8 +33,6 @@
 
 val runN = "run"
 val supported_proversN = "supported_provers"
-val kill_learnersN = "kill_learners"
-val running_learnersN = "running_learners"
 val refresh_tptpN = "refresh_tptp"
 
 (** Sledgehammer commands **)
@@ -326,8 +324,6 @@
       end
     else if subcommand = supported_proversN then
       supported_provers ctxt
-    else if subcommand = kill_learnersN then
-      kill_learners ()
     else if subcommand = unlearnN then
       mash_unlearn ()
     else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
@@ -343,8 +339,6 @@
                  [("preplay_timeout", ["0"])]))
            fact_override (#facts (Proof.goal state))
            (subcommand = learn_proverN orelse subcommand = relearn_proverN))
-    else if subcommand = running_learnersN then
-      running_learners ()
     else if subcommand = refresh_tptpN then
       refresh_systems_on_tptp ()
     else

--- 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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 02 21:15:25 2015 +0200
@@ -81,8 +81,6 @@
   val mash_weight : real
   val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
     term -> raw_fact list -> (string * fact list) list
-  val kill_learners : unit -> unit
-  val running_learners : unit -> unit
 end;
 
 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
@@ -1600,7 +1598,4 @@
       | _ => [(effective_fact_filter, mesh)])
     end
 
-fun kill_learners () = Async_Manager_Legacy.kill_threads MaShN "learner"
-fun running_learners () = Async_Manager_Legacy.running_threads MaShN "learner"
-
 end;