tuned -- cleanup before publishing assignment;

more abstract types; tuned signature;

tuned;

disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution; tuned error messages: prefer plain "error" as in document.ML;

more precise fact declarations -- fewer warnings;

global management of command execution fragments; tuned;

fully synchronized guard of running execution; tuned;

merged

added exercises

optimize isar-proofs by trying different proof methods

made SML/NJ happy

tuned

tuned;

re-assign prints of unchanged eval only -- avoid crash of new_exec;

tuned -- refrain from odd optimization;

tuned;

added "echo" command for demonstration purposes;

more abstract message channel;

explicit shutdown of message output thread;

tuned signature;

no need for raw stdin;

fall back on synchronous message output for single-threaded SML/NJ;

make SML/NJ happy;

retain main thread for protocol loop -- no access to raw ML toplevel;

removed historic dimacs2hol (see also read_dimacs_cnf_file in src/HOL/Tools/sat_solver.ML);

less intrusive token_range rendering, which is relevant for inner parse errors;

made SML/NJ happy

merged

tuned start_execution: avoid sleep on worker thread;

print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;

allow to remove print functions; tuned signature;

clarified Command.print: update old prints here;

produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);

tuned;

tuned proofs;

more formal type assign_update: avoid duplicate results and redundant update of global State.execs;

tuned message;

tuned signature -- NB: Command.read is actually part of Command.eval;

tuned protocol terminology; tuned signature;

tuned;

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;