clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;

unused;

update for release;

tuned: prefer Scala Regex operations;

tuning and updates for release;

NEWS;

discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);

give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;

merged

discontinue fragile operations;

proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);

enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);

updated documentation;

support multiple sessions, with cumulative errors; tuned command usage;

support regex patterns on messages;

support Pretty.unformatted, similar to ML version;

removed odd TODO item (see 3391a493f39a);

tuned signature;

tuned output: more Pretty.item;

tuned signature;

clarified failure: warning for logical error, exception for program breakdown;

print goal instantiation for global qed (and variations);

clarified output;

more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);