avoid double qualification for case constants

qualify more generated names with optional type name component

eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

generalized library function

updated keywords;

merged

clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt;

moved generic module to its proper place;

manage hyperlinks via PIDE editor interface;

tuned whitespace;

prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;

central management of Document.Overlays, independent of Document_Model;

tuned -- use Multi_Map;

support for maps with multiple entries per key;