| Mon, 11 Jul 2011 22:55:47 +0200 |
wenzelm |
tuned signature -- corresponding to Scala version;
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 14:09:24 +0100 |
wenzelm |
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 18:21:48 +0200 |
wenzelm |
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 11:45:42 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 11:36:12 +0200 |
wenzelm |
more uniform treatment of structure Unsynchronized in ML bootstrap phase;
|
file |
diff |
annotate
|
| Sat, 01 Aug 2009 00:09:45 +0200 |
wenzelm |
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 00:53:47 +0200 |
wenzelm |
tuned tracing;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 00:39:05 +0200 |
wenzelm |
added Multithreading.real_time;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 00:13:39 +0200 |
wenzelm |
simplified/unified Multithreading.tracing_time;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 19:38:03 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 20:53:23 +0200 |
wenzelm |
added enabled;
|
file |
diff |
annotate
|
| Thu, 02 Oct 2008 14:22:45 +0200 |
wenzelm |
max_threads_value always 1 for dummy version;
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 23:48:36 +0200 |
wenzelm |
proper values of no_interrupts, regular_interrupts;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2008 20:33:29 +0200 |
wenzelm |
removed unused sync_interrupts;
|
file |
diff |
annotate
|
| Sun, 07 Sep 2008 22:20:11 +0200 |
wenzelm |
added sync_interrupts, regular_interrupts;
|
file |
diff |
annotate
|
| Sun, 07 Sep 2008 17:46:40 +0200 |
wenzelm |
added no_interrupts;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:46 +0200 |
wenzelm |
provide dummy thread structures, including proper Thread.getLocal/setLocal;
|
file |
diff |
annotate
|
| Sat, 16 Feb 2008 16:44:00 +0100 |
wenzelm |
removed managed_process (cf. General/shell_process.ML);
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 23:22:02 +0100 |
wenzelm |
support for managed external processes;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 16:32:53 +0100 |
wenzelm |
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 21:12:02 +0100 |
wenzelm |
added get/put_data;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 22:21:42 +0100 |
wenzelm |
signature BASIC_MULTITHREADING;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 13:53:26 +0200 |
wenzelm |
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
|
file |
diff |
annotate
|