src/Pure/ML-Systems/multithreading_polyml.ML
Mon, 22 Dec 2014 20:40:37 +0100 wenzelm discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
Thu, 11 Dec 2014 23:31:30 +0100 wenzelm added Par_List in Scala, in accordance to ML version;
Wed, 26 Nov 2014 11:43:51 +0100 wenzelm load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
Thu, 12 Dec 2013 13:50:44 +0100 wenzelm simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
Wed, 11 Dec 2013 18:02:22 +0100 wenzelm support for polml-5.5.2;
Wed, 16 Jan 2013 11:31:08 +0100 wenzelm tuned comments;
Sun, 18 Nov 2012 15:38:37 +0100 wenzelm adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
Wed, 22 Aug 2012 12:07:11 +0200 wenzelm clarified bootstrapping of Pure;
Thu, 24 May 2012 15:01:17 +0200 wenzelm discontinued support for Poly/ML 5.2.1;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Tue, 08 Feb 2011 14:09:24 +0100 wenzelm added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
Sat, 05 Feb 2011 18:09:57 +0100 wenzelm clarified bootstrapping of structure TimeLimit;
Sat, 27 Nov 2010 16:29:53 +0100 wenzelm removed bash from ML system bootstrap, and past the Secure ML barrier;
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Wed, 22 Sep 2010 00:45:42 +0200 wenzelm more robust lib/scripts/process, with explicit script/no_script mode;
Mon, 20 Sep 2010 23:36:26 +0200 wenzelm refined ML/Scala bash wrapper, based on more general lib/scripts/process;
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Sun, 07 Feb 2010 20:21:38 +0100 wenzelm modernized perl scripts: prefer standalone executables;
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
Tue, 27 Oct 2009 10:54:25 +0100 wenzelm max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;
Mon, 26 Oct 2009 11:36:23 +0100 wenzelm implicit default is 4 cores -- more cost-effective;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 01 Aug 2009 00:09:45 +0200 wenzelm renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
Thu, 30 Jul 2009 23:06:06 +0200 wenzelm added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
Mon, 27 Jul 2009 17:36:30 +0200 wenzelm interruptible: Thread.testInterrupt before changing thread attributes;
Sat, 25 Jul 2009 00:53:47 +0200 wenzelm tuned tracing;
Sat, 25 Jul 2009 00:39:05 +0200 wenzelm added Multithreading.real_time;
Sat, 25 Jul 2009 00:13:39 +0200 wenzelm simplified/unified Multithreading.tracing_time;
Tue, 21 Jul 2009 23:42:29 +0200 wenzelm future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
less more (0) -50 -30 tip