Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

1. clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
2. unused;
3. update for release;
4. tuned: prefer Scala Regex operations;
5. tuning and updates for release;
6. NEWS;
7. discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);
8. give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
9. merged
10. discontinue fragile operations;
11. proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
12. enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
13. updated documentation;
14. support multiple sessions, with cumulative errors; tuned command usage;
15. support regex patterns on messages;
16. support Pretty.unformatted, similar to ML version;
17. removed odd TODO item (see 3391a493f39a);
18. tuned signature;
19. tuned output: more Pretty.item;
20. tuned signature;
21. clarified failure: warning for logical error, exception for program breakdown;
22. print goal instantiation for global qed (and variations);
23. clarified output;
24. more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);
25. clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
26. updated to postgresql-42.5.0;
27. tool to build Isabelle component for PostgreSQL JDBC;
28. clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";
29. option "show_states" for more verbosity of batch-builds;
30. tuned --- avoid warnings;
31. proper antiquotations;
32. inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;
33. proper antiquotations;
34. clarified options, following e.g. "show_consts";
35. proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;
36. unused (see 15758fced053);
37. clarified modules;
38. show goal instantiation, notably for 'schematic_goal' command (inactive by default);
39. proper umlauts;
40. tuned signature;
41. tuned signature;
42. tuned;
43. tuned;
44. tuned error message;

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

1. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
2. tuned whitespace;
3. merged
4. some slight polishing in the UTM entry
5. added congruence rule for forallM of Error-Monad
6. updated to devel
7. merged
8. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
9. removed obsolete workaround (see Isabelle/91ee232b4211);