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;

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;

clarified signature: more explicit types;

unused (see 0d30ea76756c);

tuned;

clarified signature;

tuned;

unused (see 3064e165c660);

merge

changed the order of Zipperposition slices in Sledgehammer

merged

The wellordering instantiation for length-ordered lists

show sum_list defn

prettified def

More lemmas.

Some more proofs.

a few new theorems

tuned;

clarified while-loops;

updated to postgresql-42.4.0;