Further cleaning up of messy proofs

merged

reorganisation and simplification of theorems about transcendental functions

tuned signature;

support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";

tuned whitespace;

clarified signature;

clarified signature;

tuned;

tuned;

discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);

tuned --- more robust ML patterns;

tuned;

merged

tuned signature, for the sake of AFP/Isabelle_C;

more uniform report of Markup.language_path;

omit pointless guard: ultimately observed by Isabelle_Process.report_message;

tuned signature;

clarified modules;

tuned;

tuned signature;

tuned;

tuned;

tuned output;