clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;

tuned GUI layout;

clarified GUI events, e.g. relevant for insert via completion;

more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);

common support for search field, which is actually a light-weight Highlighter;

clarified GUI focus;

more uniform detach button;

tuned signature;

renamed "Find" to "Query", with more general operations;

hardwired default_frequency to avoid fluctuation of popup content;

more visual feedback on path_completion, at the risk of file-system access in GUI painting;

tuned;

explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";

tuned GUI layout;

tuned;

some complication with ListView.Renderer to get tooltips;

expose interrupts more like ML version, but not in managed bash processes of Build;

merged

uniform Toplevel.print for all proof commands;

clarified print operations for "terms" and "theorems";

more print operations; preserve declaration order;

tuned GUI;

more decisive change of focus; more explicit Print_Item with description;

support print operations as asynchronous query;

allow empty original, e.g. path "";

more robust process kill -- postpone interrupts on current thread;

tuned signature;

tuned signature;

tuned comment

simplify selectors in code views

note correct induction schemes in 'primrec' (for N2M)

use right meson tactic for preplaying

simplify unused universally quantified variables in Z3 proofs

fixed Waldmeister endgame w.r.t. "Trueprop"

tuned structure name

added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')

renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish

added 'satx' proof method to Try0

make 'dpll_p' the default SAT solver, rather than the hard-to-get zChaff-with-proofs

added missing space between command-line options

improved whitelist (cf. be1874de8344)

renamed 'xxx_size' to 'size_xxx' for old datatype package

removed obsolete internal SAT solvers

standardize to implode_short form; clarified treatment of directories;

support for path completion based on file-system content;

yet another completion option, to imitate old less ambitious behavior;

reduced cluttering of popups;

propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);

merged

NEWS;

more robust interrupt handling for Scala_Console, which uses JVM Thread.interrupt instead of POSIX SIGINT;

more sensible interrupt of interpreter, when the user pushes Cancel button;

obsolete in scala-2.11.0;

fork Scala interpreter thread, independently of Swing_Thread;

clarified synchronization and exception handling;

more redirection;

prefer scala.Console with its support for thread-local redirection;

tuned signature -- channels for diagnostic output for system tools means stderr;

proper tool wrap-up;

tuned spelling;

avoid deprecated Scala syntax;

enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)

more standard doc session specification;

discontinued adhoc check (see also ea8343187225);

more frugal access to theory text via Reader, reduced costs for I/O text decoding; prefer non-strict Symbol.decode, since Reader[Char] may present symbols in either way;

support URLs as well;

reclaimed Byte_Reader from 51560e392e1b;

new documentation: How to Prove it

disable bad Z3 proof

use SMT2 for Boogie examples

less verbose SAT tactic

use internal proof-producing SAT solver for more efficient SMT proof replay

added internal proof-producing SAT solver

tuned output;

separate ML module

centralized upper/lowercase name mangling

optional case enforcement

obsolete: no symbol identifiers remaining in Pure

prevent subscription in nested contexts explicitly -- at foundational and user level

cleanup

NEWS

use qualified name (was interpreted as a catch-all variable name)

add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula

updated keywords;

clarified signature: load_file is still required internally;

merged

some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;

support for long names in Scala;

tuned;

Discontinued old spark_open; spark_open_siv is now spark_open

suppress slightly odd completions of "real";

tuned proofs;

tuned proofs;

clarified exit sequence: prover is reset afterwards, no more output messages;

more synchronized treatment of prover process, which might emit more messages before shutdown and requires manager to accept them;

tuned;