proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);

old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);

just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);

turned pattern unify flag into configuration option (global only);

merged

permissive uncheck -- allow printing of malformed terms (e.g. in error messages);