tuned white space;

misc tuning;

handle_result: no special treatment of outer markup (it is now properly identified by the prover); misc tuning;

single instance of rule_set;

regular activate=defer -- may debug remotely, no need to run under netbeans;

avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;

Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin; TheoryView: simplified change_receiver, only for local purposes (via command_change); Accumulator: message requires explicit prover context for now;

tuned;

tuned;

Prover: just one actor -- single message dispatch; simplified states/commands/document_versions: immutable data;

modernized Event_Bus -- based on actors; simplified Prover.keyword_decls/command_decls/completion: immutable data, eliminated decl_info; eliminated Prover.output_info; tuned;

eliminated ProverEvents.Activate -- handle "ready" within Prover; tuned prover setup; tuned;

corrected order

sidekick root data: set buffer length to avoid crash of initial caret move; separate Markup_Node, Markup_Tree, Markup_Text; added Markup_Text.flatten; Command.type_at: null-free version; eliminated Command.RootInfo; simplified printing of TypeInfo, RefInfo; added Command.content(Int, Int);

tuned color (PG 4.0);

treat all messages except status as results; report ignored status reports; invoke command.changed only for actual change; tuned;

tuned;

tuned;

replaced find_command_at by command_at -- null-free, proper Option; tuned;

tuned;

tuned;

minor tuning;

tuned MarkupNode argument order; tuned;

eliminated MarkupInfo, moved particular variants into object Command;

removed dead code;

MarkupNode: removed id;

simplified MarkupNode -- independent of Command and ProofDocument; tuned;

minor tuning;

sorted;

IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag; tuned;

tuned imports;

tuned;