src/Pure/ML-Systems/multithreading.ML
Fri, 20 Mar 2009 20:20:09 +0100 wenzelm future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
Mon, 19 Jan 2009 19:38:03 +0100 wenzelm removed Ids;
Thu, 09 Oct 2008 20:53:23 +0200 wenzelm added enabled;
Thu, 02 Oct 2008 14:22:45 +0200 wenzelm max_threads_value always 1 for dummy version;
Tue, 09 Sep 2008 23:48:36 +0200 wenzelm proper values of no_interrupts, regular_interrupts;
Mon, 08 Sep 2008 20:33:29 +0200 wenzelm removed unused sync_interrupts;
Sun, 07 Sep 2008 22:20:11 +0200 wenzelm added sync_interrupts, regular_interrupts;
Sun, 07 Sep 2008 17:46:40 +0200 wenzelm added no_interrupts;
Thu, 04 Sep 2008 16:03:46 +0200 wenzelm provide dummy thread structures, including proper Thread.getLocal/setLocal;
Sat, 16 Feb 2008 16:44:00 +0100 wenzelm removed managed_process (cf. General/shell_process.ML);
Fri, 15 Feb 2008 23:22:02 +0100 wenzelm support for managed external processes;
Wed, 02 Jan 2008 16:32:53 +0100 wenzelm added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
Thu, 20 Dec 2007 21:12:02 +0100 wenzelm added get/put_data;
Tue, 18 Dec 2007 22:21:42 +0100 wenzelm signature BASIC_MULTITHREADING;
Mon, 24 Sep 2007 13:53:26 +0200 wenzelm renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
less more (0) tip