| Tue, 17 Oct 2023 12:10:58 +0200 |
wenzelm |
tuned signature, following Isabelle/Scala;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 11:52:52 +0200 |
wenzelm |
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 11:47:13 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 15:45:06 +0200 |
wenzelm |
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 10:56:45 +0200 |
wenzelm |
distinguish proper interrupts from Poly/ML RTS breakdown;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 14:03:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 13:49:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 11:27:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 11:06:34 +0200 |
wenzelm |
more robust: avoid race condition;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 10:46:50 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2023 19:05:35 +0200 |
wenzelm |
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
|
file |
diff |
annotate
|
| Tue, 26 Sep 2023 14:42:33 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 26 Sep 2023 12:46:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 26 Sep 2023 12:30:08 +0200 |
wenzelm |
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:58:58 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:46:38 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:30:46 +0200 |
wenzelm |
clarified order of modules: early access to interrupt management of Isabelle_Threads;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:37:52 +0200 |
wenzelm |
more robust: catch/finally part is uninterruptible;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 16:17:43 +0200 |
wenzelm |
more general ML_Antiquotation.special_form;
|
file |
diff |
annotate
|
| Sun, 24 Sep 2023 15:07:40 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2023 23:45:03 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2023 17:09:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2023 17:04:56 +0200 |
wenzelm |
more robust: prefer linear data flow;
|
file |
diff |
annotate
|
| Wed, 06 Sep 2023 20:51:28 +0200 |
wenzelm |
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
|
file |
diff |
annotate
|
| Wed, 06 Sep 2023 14:09:27 +0200 |
wenzelm |
more explicit type Isabelle_Thread.T;
|
file |
diff |
annotate
|
| Mon, 04 Sep 2023 21:03:13 +0200 |
wenzelm |
discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785);
|
file |
diff |
annotate
|
| Sun, 24 May 2020 20:59:34 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 13:24:12 +0200 |
wenzelm |
clarified signature: more uniform ML vs. Scala;
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 13:19:29 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 13:05:40 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
| base
|