tuned signature -- more robust;

tuned signature;

clarified signature: Export.Provider knows its (accidental) theory_names;

clarified signature;

tuned, following hints by IntelliJ IDEA;

clarified signature: proper session_name for Sessions.Base (like Sessions.Info);

tuned signature;

clarified signature;

clarified signature;

clarified signature;

avoid multiple load_commands;

avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2);

tuned signature -- avoid redundant arguments;

tuned -- following hints by IntelliJ IDEA;

tuned signature;

tuned comments;

removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);

tuned signature;

clarified signature;

clarified signature: avoid repeated db_context.input_database;

clarified signature: more robust;

removed somewhat pointless operations (see a6c69599ab99);

clarified signature;

tuned;

tuned;

clarified signature;

clarified names;

clarified signature;

clarified names;

clarified signature;