| Tue, 02 Apr 2024 17:20:09 +0200 |
wenzelm |
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;
|
file |
diff |
annotate
|
| Tue, 26 Sep 2023 14:42:33 +0200 |
wenzelm |
clarified signature;
|
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
|
| Tue, 09 May 2023 20:32:49 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 16:31:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 08 May 2023 23:30:58 +0200 |
wenzelm |
support for cached evaluation via weak_ref;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2018 14:01:52 +0200 |
wenzelm |
updated to polyml-5.7.1-7 (see also afa7c5a239e6);
|
file |
diff |
annotate
|
| Fri, 06 Jul 2018 15:35:48 +0200 |
wenzelm |
more frugal assignment of lazy value: fewer mutexes, condvars;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 16:58:39 +0200 |
wenzelm |
eliminated unused argument;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 14:00:23 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 11:21:38 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 17:16:30 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Dec 2014 22:10:09 +0100 |
wenzelm |
back to full synchronization (cf. eb3e399f5b9f);
|
file |
diff |
annotate
|
| Thu, 18 Dec 2014 16:13:54 +0100 |
wenzelm |
peek value without synchronization;
|
file |
diff |
annotate
|
| Fri, 12 Dec 2014 14:31:57 +0100 |
wenzelm |
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 11:43:51 +0100 |
wenzelm |
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 12:09:55 +0200 |
wenzelm |
synchronized access, similar to ML version;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 00:27:06 +0200 |
wenzelm |
more uniform synchronized variables;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 23:10:18 +0200 |
wenzelm |
more uniform Counter in ML and Scala;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 22:55:47 +0200 |
wenzelm |
tuned signature -- corresponding to Scala version;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 16:13:37 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 21:44:19 +0100 |
wenzelm |
added general Synchronized.counter convenience;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 22:05:02 +0100 |
wenzelm |
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 15:19:44 +0200 |
wenzelm |
support single-assigment variables -- based on magic RTS operations by David Matthews;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 22:46:10 +0200 |
wenzelm |
Synchronized.value does not require locking, since assigments are atomic;
|
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
|
| Tue, 28 Jul 2009 15:05:18 +0200 |
wenzelm |
added unsynchronized Synchronized.peek;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 19:38:03 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Tue, 14 Oct 2008 13:01:56 +0200 |
wenzelm |
added value;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2008 15:48:40 +0200 |
wenzelm |
State variables with synchronized access.
|
file |
diff |
annotate
|