src/Pure/Isar/toplevel.ML
2015-04-04 ago support private scope for individual local theory commands;
2015-01-29 ago discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2014-12-23 ago explicit message channels for "state", "information";
2014-12-19 ago tuned;
2014-11-26 ago more informative failure of protocol commands, with exception trace;
2014-11-22 ago tuned;
2014-11-13 ago uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
2014-11-06 ago more explicit Keyword.keywords;
2014-11-03 ago eliminated unused int_only flag (see also c12484a27367);
2014-10-31 ago discontinued pointless option: timing is always on (overall theory only);
2014-10-31 ago eliminated odd flags and hook;
2014-10-28 ago 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28 ago tuned;
2014-07-02 ago centralized (ad-hoc) switching of targets in named_target.ML
2014-06-07 ago avoid odd Named_Target.reinit altogether
2014-06-07 ago clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-05-12 ago smarter recovery from toplevel type error;
2014-05-07 ago print results as "state", to avoid intrusion into the source text;
2014-05-07 ago discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-07 ago tuned;
2014-05-06 ago clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-05 ago more print operations;
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-14 ago prefer more robust Synchronized.var;
2014-03-12 ago more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
2014-03-11 ago slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;
2014-02-13 ago tuned whitespace;
2013-12-05 ago more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
2013-11-11 ago tuned signature;
2013-09-18 ago improved printing of exception trace in Poly/ML 5.5.1;
2013-09-04 ago some explicit indication of Proof General legacy;
2013-08-25 ago maintain goal forks as part of global execution;
2013-08-25 ago discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
2013-07-30 ago type theory is purely value-oriented;
2013-07-18 ago immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-09 ago tuned message;
2013-07-05 ago tuned signature;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-07-02 ago clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-05-22 ago mark local theory as brittle also after interpretation inside locales;
2013-04-23 ago brittleness stamping for local theories
2013-04-09 ago just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09 ago clarified protocol_message undefinedness;
2013-04-09 ago discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-03 ago more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-02 ago more centralized command timing;
2013-03-27 ago extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27 ago explicit Toplevel.is_skipped_proof;
2013-03-27 ago more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-13 ago clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
2013-03-04 ago refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-03-03 ago uniform treatment of global/local proofs;
2013-03-03 ago tuned;
2013-03-03 ago clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-03-03 ago more Thy_Syntax.element operations;
2013-02-28 ago simplified Proof.future_proof;
2013-02-26 ago tuned signature;
2013-02-26 ago fork diagnostic commands (theory loader and PIDE interaction);