more markup for improper elements;

tuned signature;

unused;

tuned signature -- rearranged modules;

tuned proofs;

back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;

remove unnecessary finiteness assumptions from lemmas about setsum