# HG changeset patch
# User wenzelm
# Date 1223046459 -7200
# Node ID 855ca2dcc03da1884a5a9d90fe5c9e7c1fa664be
# Parent  9339d4dcec8b48d72c56649ceaf52a9ada4debe6
simplified thread creation via SimpleThread;
managing_thread: option type (fork of inactive thread assumes threads are available in the first place);

diff -r 9339d4dcec8b -r 855ca2dcc03d src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Fri Oct 03 16:37:09 2008 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Fri Oct 03 17:07:39 2008 +0200
@@ -60,7 +60,7 @@
   val lock = Mutex.mutex () (* to be aquired for changing state *)
   val state_change = ConditionVar.conditionVar () (* signal when state changes *)
   (* watches over running threads and interrupts them if required *)
-  val managing_thread = ref (Thread.fork (fn () => (), []))
+  val managing_thread = ref (NONE: Thread.thread option);
 
   (* move a thread from active to cancelling
     managing_thread trys to interrupt all threads in cancelling
@@ -77,7 +77,7 @@
   (* must *not* be called more than once!! => problem with locks *)
   fun start () =
     let
-    val new_thread = Thread.fork (fn () =>
+    val new_thread = SimpleThread.fork false (fn () =>
       let
       (* never give up lock except for waiting *)
       val _ = Mutex.lock lock
@@ -111,16 +111,17 @@
           in
             wait_for_next_event next_time
           end
-        in wait_for_next_event Time.zeroTime end,
-        [Thread.InterruptState Thread.InterruptDefer])
-      in managing_thread := new_thread end
+        in wait_for_next_event Time.zeroTime end)
+      in managing_thread := SOME new_thread end
 
   (* calling thread registers itself to be managed here with a relative timeout *)
   fun register birthtime deadtime (thread, name) =
     let
     val _ = Mutex.lock lock
     (* create the atp-managing-thread if this is the first call to register *)
-    val _ = if Thread.isActive (! managing_thread) then () else start ()
+    val _ =
+      if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+      then () else start ()
     (* insertion *)
     val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread))
     val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread))