clarified margin operations (again, reverting 4794576828df);

clarified modules;

more reactive interrupts (via Future.cancel);

Document.Snapshot: support for multiple snippet_commands; clarified Command.rich_text: prefer explicit id, e.g. from message serial; clarified Pretty_Text_Area.update: Protocol_Message.provide_serial; clarified Pretty_Text_Area.format_rich_texts, with separate formatting of messages;

more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;

clarified signature: include standard margin in object equality;

performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);

The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2

merged

merged

clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);

clarified signature;

tuned GUI: avoid wasting space with proportional fonts;

clarified signature;

more accurate pretty_margin for proportional fonts;

clarified signature: more uniform;

tuned: fewer warnings in IntelliJ IDEA;

tuned signature;

tuned signature;

clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;

more accurate message boundaries;

tuned whitespace;

clarified signature: more robust type XML.Elem;

clarified signature;

clarified signature;

clarified output representation: postpone Pretty.separate;

tuned;

tuned: fewer warnings in IntelliJ IDEA;

clarified signature: more accurate types;

tuned signature: more standard names;