reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

gracefully handle empty SPASS problems

pass sound option to Sledgehammer tactic

tuned signature -- contrast physical output primitives versus Output.raw_message;

tuned signature;

discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

some support for toplevel printing wrt. editor perspective (still inactive);

propagate editor perspective through document model;

some support for editor perspective;

discontinued redundant Edit_Command_ID;

reduced warnings;

tuned message;