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;