isabelle: File revisions

src/Pure/Concurrent/future.ML

Tue, 14 May 2013 20:46:09 +0200	wenzelm	more uniform Markup.print_real;	file \| diff \| annotate
Tue, 09 Apr 2013 15:59:02 +0200	wenzelm	clarified protocol_message undefinedness;	file \| diff \| annotate
Mon, 08 Apr 2013 15:44:09 +0200	wenzelm	discontinued odd magic number, which was once used for performance measurements;	file \| diff \| annotate
Tue, 05 Mar 2013 11:37:01 +0100	wenzelm	removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);	file \| diff \| annotate
Sun, 03 Mar 2013 17:34:42 +0100	wenzelm	more uniform Future.map: always internalize failure;	file \| diff \| annotate
Tue, 26 Feb 2013 13:38:34 +0100	wenzelm	disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;	file \| diff \| annotate
Tue, 26 Feb 2013 13:05:48 +0100	wenzelm	signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;	file \| diff \| annotate

isabelle