more generic button;

support for query operations that consist of parallel segments;

more tooltips;

tuned -- more explicit type Status.Value;

more explicit status for query operation; avoid output with outdated snapshot; animation rate according to status; added PIDE.document_snapshot convenience -- independent of availability of physical buffer;

tuned signature;

query process animation;

tuned signature;

tuning

tuning

tuning

tuning

export ML function (for primcorec)

more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;

tuned proofs;