#
ba771aa0 |
|
04-Dec-2019 |
wenzelm <none@none> |
clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into Isabelle/jEdit;
|
#
0f5977d1 |
|
20-Nov-2019 |
wenzelm <none@none> |
tuned signature;
|
#
4e527efd |
|
20-Nov-2019 |
wenzelm <none@none> |
support for bulk operations: consume mailbox content in batches;
|
#
8d509979 |
|
19-Nov-2019 |
wenzelm <none@none> |
clarified signature -- more explicit types;
|
#
9bd022db |
|
16-Jun-2017 |
wenzelm <none@none> |
more general dispatcher operations;
|
#
3ee6c0a8 |
|
23-Oct-2016 |
wenzelm <none@none> |
discontinued unused / untested distinction of separate PIDE modules;
|
#
ebff3653 |
|
03-Nov-2015 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala
|
#
9595dab4 |
|
27-Jun-2014 |
wenzelm <none@none> |
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
|
#
3be931d9 |
|
29-Apr-2014 |
wenzelm <none@none> |
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
|
#
f8ba67c4 |
|
25-Apr-2014 |
wenzelm <none@none> |
replaced manager Actor by Consumer_Thread, which is lazy to defer its start to actual Handler init time;
|
#
00bba9f1 |
|
24-Apr-2014 |
wenzelm <none@none> |
misc tuning;
|
#
2be4980a |
|
24-Apr-2014 |
wenzelm <none@none> |
support for requests with explicit acknowledgment (and exception propagation);
|
#
8d6b068c |
|
24-Apr-2014 |
wenzelm <none@none> |
more robust thread: continue after failure;
|
#
4ef102af |
|
24-Apr-2014 |
wenzelm <none@none> |
allow more control of main loop; more robust is_active test, although thread could terminate at any time;
|
#
09e4df88 |
|
24-Apr-2014 |
wenzelm <none@none> |
more robust shutdown; less ooddities;
|
#
d82d631d |
|
24-Apr-2014 |
wenzelm <none@none> |
consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
|