# HG changeset patch
# User wenzelm
# Date 1415023695 -3600
# Node ID 4479722497859ff49caab5766e22b102103d7d36
# Parent  9e0ecb66d6a74204beee23509ddb9c30ffd33f51
clarified legacy code;

diff -r 9e0ecb66d6a7 -r 447972249785 src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon Nov 03 14:50:27 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Mon Nov 03 15:08:15 2014 +0100
@@ -4,10 +4,10 @@
     Author:     Jasmin Blanchette, TU Muenchen
 
 Central manager for asynchronous diagnosis tool threads.
+
+Proof General legacy!
 *)
 
-(*Proof General legacy*)
-
 signature ASYNC_MANAGER =
 sig
   val break_into_chunks : string -> string list
@@ -22,6 +22,14 @@
 structure Async_Manager : ASYNC_MANAGER =
 struct
 
+fun make_thread interrupts body =
+  Thread.fork
+    (fn () =>
+      Runtime.debugging NONE body () handle exn =>
+        if Exn.is_interrupt exn then ()
+        else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
+      Simple_Thread.attributes interrupts);
+
 val message_store_limit = 20
 val message_display_limit = 10
 
@@ -111,7 +119,7 @@
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
-    else let val manager = SOME (Runtime.thread false (fn () =>
+    else let val manager = SOME (make_thread false (fn () =>
       let
         fun time_limit timeout_heap =
           (case try Thread_Heap.min timeout_heap of
@@ -160,7 +168,7 @@
   check_thread_manager ())
 
 fun thread tool birth_time death_time desc f =
-  (Runtime.thread true
+  (make_thread true
        (fn () =>
            let
              val self = Thread.self ()
diff -r 9e0ecb66d6a7 -r 447972249785 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Nov 03 14:50:27 2014 +0100
+++ b/src/Pure/Isar/runtime.ML	Mon Nov 03 15:08:15 2014 +0100
@@ -22,7 +22,6 @@
   val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
   val toplevel_program: (unit -> 'a) -> 'a
-  val thread: bool -> (unit -> unit) -> Thread.thread
 end;
 
 structure Runtime: RUNTIME =
@@ -166,14 +165,5 @@
 fun toplevel_program body =
   (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
 
-(*Proof General legacy*)
-fun thread interrupts body =
-  Thread.fork
-    (fn () =>
-      debugging NONE body () handle exn =>
-        if Exn.is_interrupt exn then ()
-        else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn),
-      Simple_Thread.attributes interrupts);
-
 end;