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;
2012-08-30 ago tuned signature;
2012-08-29 ago tuned signature;
2012-08-29 ago renamed Position.str_of to;
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;