more precise notion of bad messages;

use Text_Edit provided by Isabelle;

result.is_ready is not bad;

singleton status messages, with more precise patterns -- report bad messages;

back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
recent_document: require finished state assignment;
explicitly typed Session.lookup_command;

slightly more uniform/robust handling of visible document;
uniform changed_delay for view updates;
misc tuning;

recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
Change.ancestors: frugal iterator;

more explicit treatment of command/document state;
misc tuning and clarification;

removed unused document_change bus;

tuned;