allow whitespace in file names;

tuned;

more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;

allow worker guest threads, which participate actively in future joins, but are outside thread accounting;

made SML/NJ happy

completely rewrote SH compress; added two parameters for experimentation/fine grained control

moved code -> easier debugging

tuned proofs

some support for Cygwin;

reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;

tuned signature;

discontinued obsolete "isabelle print";

discontinued command 'print_drafts';

some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;

removed pointless / outdated keywords, superseded by specific Token_Markup.Marker;

tuned comments;

Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)

tuned spelling

eliminated pointless catch of unlikely exceptions, which may occur in Doc.contents already;

more release notes according to availability in proper release vs. repository clone; discontinued generated HTML for files that are accessible in 1 click;

quick access to release notes (imitating website/documentation.html);

more dependencies;

minimal jedit mode for Isabelle NEWS;

merged

more uniform Counter in ML and Scala;

tuned signature; tuned comments;

tuned signature -- eliminated pointless type synonym;

tuned signature; tuned;

clarified type Command.eval;

tuned signature;

tuned signature;

explicit module Document_ID as source of globally unique identifiers across ML/Scala;

improved proof automation for numerals

merged

separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;

more Command.memo operations; more explicit types Command.eval vs. Command.print vs. Document.exec; clarified print function parameters;

tund proofs

tuned;

made SML/NJ happy;

merged

more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering

consider explicit hint for domain of class parameters when printing instance statements

explicit hint for domain of class parameters in instance statements

merged

tuned message;

more exception handling -- make print functions total;

more print function parameters; check command_visible statically in assignment, instead of dynamically in execution;

tuned;

discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;

tuned;

allow multiple print functions;

tuned signature;

tuned signature;

tuned;

tuned signature;

use long goal format in rel_induct theorem

share some code between codatatypes, datatypes and eventually prim(co)rec

tuned names

tuned;

allow choice of target directory (again, see also 58e2d0cd81ae);

postinstall: recover Cygwin permissions;

clarified initial cd;

clarified Proofterm.proofs vs. Goal.skip_proofs;

clarified focus after dismiss;

tuned signature;

avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);

more robust delayed invocation;

clarified tooltip timing of pending event and active state;

less intrusive border, notably on windows;

tighten tooltip size;

visually explicit focus (behaviour dependent on platform and look-and-feel);

tuned;

more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;

discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;

backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;

just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;

CONTRIBUTORS

avoid potential race condition of focusLost/dismiss vs. popup.show;

more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;

explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;

update text only once;

tuned signature;

more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;

manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6); more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory; auxiliary geometry measurement via single hidden window; tuned signature;

tuned signature;

yet another warning

sort out code equations headed by a projection of a abstract datatype

formally accept dictionary parameters for constants on left hand sides in equations

do not choke on type variables emerging during rewriting

load icons via options -- prefer IntelliJ IDEA for now;

support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);

manage option "proofs" within theory context -- with minor overhead for primitive inferences;

tuned signature;

proper bold versions of 00ac (logicalnot), 00b0 (degree);

tuned signature;

merged