JEDIT_JAVA_OPTIONS: actors.enableForkJoin=false is supposed to enable ResizableThreadPoolScheduler, to avoid starvation of excessive amounts of future tasks etc.;

session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;

session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;

use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;

Swing_Thread.now: volatile result to make double-sure;

Document_Model.token_marker: misc tuning and simplification;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; Markup_Tree.select: plain Iterator; misc tuning and simplification;

XML.Cache: intern property keys once and for all (again);

more careful locking of jEdit buffer;

avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;