tuned proofs -- fewer warnings;

simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;

discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;

some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1); tuned;

use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);

tuned proofs;

tuned proofs;