| Wed, 17 Oct 2012 21:18:32 +0200 |
wenzelm |
more robust cancel_now: avoid shooting yourself in the foot;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 15:17:24 +0200 |
wenzelm |
more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 21:51:34 +0200 |
wenzelm |
tuned white-space;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:20:27 +0200 |
wenzelm |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 00:09:15 +0100 |
wenzelm |
admit dummy implementation;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 23:15:15 +0100 |
wenzelm |
exported SimpleThread.attributes;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 11:25:56 +0100 |
wenzelm |
SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
|
file |
diff |
annotate
|
| Sat, 01 Aug 2009 00:09:45 +0200 |
wenzelm |
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
|
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
|
| Sat, 18 Jul 2009 22:45:33 +0200 |
wenzelm |
synchronized: tuned tracing;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 19:38:03 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2008 15:48:39 +0200 |
wenzelm |
added generic combinator for synchronized evaluation (formerly in future.ML);
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 20:53:17 +0200 |
wenzelm |
added fail-safe interrupt;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 15:37:32 +0200 |
wenzelm |
Simplified thread fork interface.
|
file |
diff |
annotate
|