tuned -- more robust against changes;

more robust: avoid race-condition of terminated vs. consolidated;

do not expose obscure flags;

clarified quasi_consolidated state: ensure that exports are present for ok nodes;

clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;

tuned documentation;

more detailed node_status;

clarified bracketing of messages: [forked [running finished] joined];

NEWS;

clarified reset_notepad;

more robust reset_state: begin/end structure takes precedence over goal/proof structure;

no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;

clarified signature;

tuned;

clarified message;

updated version;

more explicit status for "canceled" command within theory node;

back to post-release mode;

clarified message;

more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;

more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);

tuned;

support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;

clarified signature: proper typargs;

merged

export locale content; read_theory_names: proper classrel, arities; tuned signature;

tuned;

Some basic materials on filters and topology

merged

more accurate position for auxiliary files;

clarified signature;

tuned;