clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

theory_name based on session_directories: no need for expensive all_known;

clarified session_directories: relative to session_path, with overlapping information;

clarified signature: retain global session information, unaffected by later restriction;

disable fragile options for now;

avoid overlapping session directories;

support for explicit session directories;

obsolete (see 94442fce40a5);

optional trace output;

prefer commands_accepted: fewer protocol messages;

prefer define_commands_bulk: fewer protocol messages;

clarified signature;