src/Pure/Isar/toplevel.ML
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);
2010-08-12 ago named target is optional; explicit Name_Target.reinit
2010-08-12 ago Named_Target.init: empty string represents theory target
2010-08-12 ago Named_Target.theory_init
2010-08-11 ago merged
2010-08-11 ago avoid arcane Local_Theory.reinit entirely
2010-08-11 ago merged
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
2010-08-11 ago removed obsolete Toplevel.enter_proof_body;
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-27 ago simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
2010-07-25 ago simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-24 ago tuned;
2010-07-24 ago moved basic thy file name operations from Thy_Load to Thy_Header;
2010-07-24 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-07-22 ago tuned signature;
2010-07-22 ago eliminated some unreferenced identifiers;
2010-07-22 ago tuned;
2010-07-21 ago clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 ago avoid duplicate printing of 'theory' state (cf. 173974e07dea);