src/Pure/Isar/toplevel.ML
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;
2011-01-13 ago Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2010-12-04 ago formal notepad without any result;
2010-10-25 ago renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-17 ago discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-10 ago avoid extra wrapping for interrupts;
2010-09-09 ago removed dead code;
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-31 ago moved Toplevel.run_command to Pure/PIDE/document.ML;
2010-08-30 ago Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
2010-08-30 ago tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-25 ago added some proof state markup, notably number of subgoals (e.g. for indentation);