find theory files via session structure: much faster Prover IDE startup;

find theory node name via session directories;

disallow overlapping session directories;

tidied up some massive ugliness

clarified messages;

clarified syntax: 'directories' and 'theories' belong together;

more documentation;

check session directories;

declare session directories;

clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

theory_name based on session_directories: no need for expensive all_known;

clarified session_directories: relative to session_path, with overlapping information;

clarified signature: retain global session information, unaffected by later restriction;

disable fragile options for now;

avoid overlapping session directories;

support for explicit session directories;

obsolete (see 94442fce40a5);

optional trace output;

prefer commands_accepted: fewer protocol messages;

prefer define_commands_bulk: fewer protocol messages;

clarified signature;

tuned signature -- prefer bulk messages;

tuned signature;

proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);

more robust;

unused;

proper finished_theory status for result;

more central checkpoint;

disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;

merged

load theories in stages, to reduce ML heap requirements;

more complete graph;

tuned messages;

tuned signature;

clarified signature;

tuned important special case;

tuned signature;

more dump_checkpoints;

clarified signature;

clarified state variable: avoid extra mutability via Promise;

Removal of the redundant ancestor Continuous_Extension

Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.

Theory Derivative no longer depends on Path_Connected

more explicit type Dump.Session, with context information;

proper orientation;

clarified signature: prefer operations without position;

prefer Theory_Ordering theory names are unique (due to proper session context);

clarified signature: full dependency graph;