src/Pure/Isar/toplevel.ML
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);
2013-02-26 ago tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;
2013-02-26 ago tuned;
2013-02-25 ago discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2013-02-25 ago clarified Toplevel.element_result: scheduling policies happen here;
2013-02-24 ago simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
2013-02-22 ago make SML/NJ happy;
2013-02-22 ago eliminated hard tabs;
2013-02-21 ago highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
2013-02-20 ago more tight representation of command timing;
2013-02-20 ago proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
2013-02-19 ago improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-02-19 ago suppress timing message in full PIDE protocol -- this is for batch build;
2013-02-19 ago support for prescient timing information within command transactions;
2013-02-19 ago emit command_timing properties into build log;
2013-01-16 ago tuned signature;
2013-01-05 ago more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-16 ago more informative errors for 'proof' and 'apply' steps;
2012-09-01 ago discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 ago more precise register_proofs for local goals;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30 ago some support for registering forked proofs within Proof.state, using its bottom context;