src/Pure/Isar/toplevel.ML
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;
2012-08-30 ago tuned signature;
2012-08-29 ago tuned signature;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-11 ago vacuous execution after first malformed command;
2012-08-01 ago recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
2012-05-17 ago tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
2012-04-11 ago clarified proof_result: finish proof formally via head tr, not end_tr;
2012-04-10 ago misc tuning and simplification;
2012-04-10 ago static relevance of proof via syntax keywords;
2012-04-02 ago misc tuning and simplification;
2012-03-21 ago more explicit Toplevel.open_target/close_target;
2012-03-16 ago defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-14 ago pass positions for named targets, for formal links in the document model;
2011-08-19 ago maintain recent future proofs at transaction boundaries;
2011-08-18 ago more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-15 ago tuned error message;
2011-08-13 ago clarified Toplevel.end_theory;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 ago provide node header via Scala layer;
2011-07-05 ago get theory from last executation state;
2011-07-05 ago explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
2011-07-05 ago tuned signature;
2011-04-16 ago modernized structure Proof_Context;
2011-03-26 ago present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-02-04 ago parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2011-01-31 ago tuned signature;
2011-01-31 ago support named tasks, for improved tracing;