commands with overlay remain visible, to avoid loosing printed output;

initial update of nodes_required, for proper GUI state;

tuned signature;

avoid repeated PIDE.flush_buffers when manipulating overlays;

tuned proofs;

merged

some actual find_theorems functionality;

more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);

prefer canonical order, to avoid potential fluctuation due to front-end edits;

tuned signature;

minimal print function "find_theorems", which merely echos its arguments;

support print functions with explicit arguments, as provided by overlays;

maintain overlays within node perspective; tuned signature;

some tracking of command location; tuned;

tuned proofs;

dockable window for "find" dialog (GUI only);

tuned;

more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)

more (co)datatype docs

tuned exercises

more (co)datatype documentation

more (co)datatype documentation

store relator induction in fp_result

merged

optional static analysis for Poly/ML 5.5.x;

exception trace for Poly/ML 5.5.1, using regular Isabelle output;

recode utf8 for ML, as done in feeder.pl;

more explicit read-only non-TTY mode;

clarified options;

specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;