# HG changeset patch # User wenzelm # Date 1221572253 -7200 # Node ID f978c8e75118861f18540148af9a76b7d3170928 # Parent de20fccf65096c3ab97f61be59fbdfe8ef7c50cd SimpleThread.fork; diff -r de20fccf6509 -r f978c8e75118 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Tue Sep 16 15:37:32 2008 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Sep 16 15:37:33 2008 +0200 @@ -160,8 +160,7 @@ | SOME work => (execute name work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) - change workers - (cons (Thread.fork (fn () => worker_loop name, Multithreading.no_interrupts), true)); + change workers (cons (SimpleThread.fork false (fn () => worker_loop name), true)); (* scheduler *) @@ -203,8 +202,7 @@ fun scheduler_check () = SYNCHRONIZED "scheduler_check" (fn () => if not (scheduler_active ()) then - (do_shutdown := false; - scheduler := SOME (Thread.fork (scheduler_loop, Multithreading.no_interrupts))) + (do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop)) else if ! do_shutdown then error "Scheduler shutdown in progress" else ()); diff -r de20fccf6509 -r f978c8e75118 src/Pure/Concurrent/schedule.ML --- a/src/Pure/Concurrent/schedule.ML Tue Sep 16 15:37:32 2008 +0200 +++ b/src/Pure/Concurrent/schedule.ML Tue Sep 16 15:37:33 2008 +0200 @@ -53,12 +53,8 @@ (*pool of running threads*) val status = ref ([]: exn list); val running = ref ([]: Thread.thread list); - fun start f = - (inc active; - change running (cons (Thread.fork (f, Multithreading.no_interrupts)))); - fun stop () = - (dec active; - change running (filter (fn t => not (Thread.equal (t, Thread.self ()))))); + fun start f = (inc active; change running (cons (SimpleThread.fork false f))); + fun stop () = (dec active; change running (remove Thread.equal (Thread.self ()))); (*worker thread*) fun worker () = diff -r de20fccf6509 -r f978c8e75118 src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Tue Sep 16 15:37:32 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.ML Tue Sep 16 15:37:33 2008 +0200 @@ -118,10 +118,10 @@ val path = File.platform_path (Path.explode out); val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*) val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*) - val _ = Thread.fork (auto_flush TextIO.stdOut, Multithreading.no_interrupts); + val _ = SimpleThread.fork false (auto_flush TextIO.stdOut); in out_stream end; - val _ = Thread.fork (auto_flush out_stream, Multithreading.no_interrupts); - val _ = Thread.fork (auto_flush TextIO.stdErr, Multithreading.no_interrupts); + val _ = SimpleThread.fork false (auto_flush out_stream); + val _ = SimpleThread.fork false (auto_flush TextIO.stdErr); in Output.writeln_fn := message out_stream "A" Markup.writelnN; Output.priority_fn := message out_stream "B" Markup.priorityN;