afford default cache policy, despite 6a29709906c6;

tuned signature;

clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;

tuned;

tuned signature;

clarified signature;

clarified modules;

merged

tuned;

clarified message;

clarified signature: prefer Export.Session_Context over Sessions.Database_Context; discontinued obsolete operations;

clarified signature: prefer Export.Context;

clarified signature: find session_database within Session_Context.db_hierarchy;

clarified signature: prefer Export.Session_Context;

prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;

clarified signature;

tuned signature, following hints by IntelliJ IDEA;

clarified signature: more robust treatment of server;

discontinued Export.Provider in favour of Export.Context and its derivatives; uniform treatment of all sessions, including Pure;

clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;

tuned signature: more operations;

misc tuning and clarification;

clarified Document.Snapshot.all_exports: refer to material from this (virtual) session; clarified treatment of Session_Context.theory_names, added export_names; clarified treatment of document_snapshot: sites on top of the session_stack;

clarified database query: refer to semantic theories;

clarified signature: more operations;

clarified signature: persistent theory_names in lexical order;

proper session_databases for database_server: need to follow precise session_hierarchy;

redundant;

clarified signature: more robust close operation;

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