clarified signature: more robust close operation;

more uniform exports: proper encoding of empty parents for Pure;

clarified signature: more uniform treatment of empty exports;

clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;

more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log); removed unused imports_hierarchy;

clarified context for retrieval: more explicit types, with optional close() operation;

tuned;

unused;

retrieve information about used files;

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;