silenced subsumption warnings for default code equations entirely

merged

NEWS; tuned description;

tuned proofs;

updated key bindings to execution range;

traverse node on change of "required" state;

keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;

maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;

afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;

clarified conditions for node traversal;

tuned;

pro-forma Goal.reset_futures, despite lack of final join/commit;

tuned;

tuned;

back to model.update_perspective with delay (cf. a20631db9c8a);

show displaced messages (e.g. from protocol thread) as raw output;

actually purge removed goal futures -- avoid memory leak;

tuned -- less redundant data structure;

always init GUI state;

tuned signature;

discontinued notion of "stable" result -- running execution is never canceled;

obsolete;

support declarative editor_execution_range, instead of old-style check/cancel buttons;

avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference

updated Sledgehammer prover versions

parse nonnumeric identifiers in E proofs correctly

simplified Vampire hack -- no need to run it for other ATPs

added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")

prefer examples that work out of the box;

breakable @{file};