src/Pure/Isar/toplevel.ML
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);
2010-07-20 ago toplevel pp for Proof.state and Toplevel.state;
2010-07-20 ago Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
2010-07-20 ago eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
2010-07-05 ago async_state: report within proper transaction context;
2010-07-04 ago general Future.report -- also for Toplevel.async_state;
2010-07-03 ago run_command: actually observe "print" flag;
2010-07-03 ago Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-31 ago Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-04-26 ago proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
2010-04-23 ago added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-02-18 ago removed unused Theory_Target.begin;
2009-11-17 ago init_theory: Runtime.controlled_execution for proper exception trace etc.;
2009-11-17 ago implicit name space grouping for theory/local_theory transactions;
2009-11-13 ago modernized structure Local_Theory;
2009-11-10 ago Toplevel.thread provides Isar-style exception output;
2009-11-10 ago modernized structure Theory_Target;