isabelle update -u control_cartouches;

prefer control symbol antiquotations;

tuning punctuation in messages output by Isabelle

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

clarified modules;
tuned signature;

explicit error for Toplevel.proof_of;
eliminated obsolete Toplevel.unknown_proof;
more total Toplevel.proof_position_of;

@{command_spec} is superseded by @{command_keyword};

tuned signature -- prefer qualified names;

explicit message channels for "state", "information";
separate state_message_color;

allow diagnostic proof commands with skip_proofs;

more explicit Keyword.keywords;

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

eliminated obsolete Proof.goal_message -- print outcome more directly;

eliminated odd flags and hook;

discontinued obsolete Output.urgent_message;

discontinued Proof General;

more uniform ML/document antiquotations;

avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);

added Theory.setup convenience;

explicit "strict" flag for print functions (flipped internal meaning);
non-strict query operations may operate on failed states;

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

tuned signature;

avoid spurious warnings, notably of 'try0' about already declared simps etc.;

initial delay for automatically tried tools;

tuned;

determine print function parameters dynamically, e.g. depending on runtime options;

clarified some default options;

gutter icon for information messages;
avoid redundant Pretty.chunks to keep Markup.information node topmost;

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

system options for Isabelle/HOL proof tools;

clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;

maintain ProofGeneral preferences within ProofGeneral module;
initialize Isabelle/Pure preferences within normal user space (with antiquotations);
tuned;

just one ProofGeneral module;

--HG--
rename : src/Pure/ProofGeneral/proof_general_emacs.ML => src/Pure/ProofGeneral/proof_general.ML

got rid of legacy smartness

more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);

outer syntax command definitions based on formal command_spec derived from theory header declarations;

make SML/NJ happy

repaired theory merging and defined/used helpers

prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

handle non-auto try case of Sledgehammer better

added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

renamed "Auto_Tools" "Try"

--HG--
rename : src/Tools/auto_tools.ML => src/Tools/try.ML