src/Pure/Isar/toplevel.ML
2011-01-13 wenzelm 2011-01-13 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-17 wenzelm 2010-09-17 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 wenzelm 2010-09-10 avoid extra wrapping for interrupts;
2010-09-09 wenzelm 2010-09-09 removed dead code;
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-31 wenzelm 2010-08-31 moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;
2010-08-30 wenzelm 2010-08-30 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.; simplified Toplevel.error_msg;
2010-08-30 wenzelm 2010-08-30 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-25 wenzelm 2010-08-25 added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;
2010-08-12 haftmann 2010-08-12 named target is optional; explicit Name_Target.reinit
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 avoid arcane Local_Theory.reinit entirely
2010-08-11 wenzelm 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-11 wenzelm 2010-08-11 removed obsolete Toplevel.enter_proof_body;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-27 wenzelm 2010-07-27 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; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;
2010-07-25 wenzelm 2010-07-25 simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-24 wenzelm 2010-07-24 tuned;
2010-07-24 wenzelm 2010-07-24 moved basic thy file name operations from Thy_Load to Thy_Header;
2010-07-24 wenzelm 2010-07-24 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
2010-07-22 wenzelm 2010-07-22 tuned signature;
2010-07-22 wenzelm 2010-07-22 eliminated some unreferenced identifiers;
2010-07-22 wenzelm 2010-07-22 tuned;
2010-07-21 wenzelm 2010-07-21 clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 wenzelm 2010-07-20 avoid duplicate printing of 'theory' state (cf. 173974e07dea);
2010-07-20 wenzelm 2010-07-20 toplevel pp for Proof.state and Toplevel.state;
2010-07-20 wenzelm 2010-07-20 Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
2010-07-20 wenzelm 2010-07-20 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; tuned some error messages;
2010-07-05 wenzelm 2010-07-05 async_state: report within proper transaction context;
2010-07-04 wenzelm 2010-07-04 general Future.report -- also for Toplevel.async_state;
2010-07-03 wenzelm 2010-07-03 run_command: actually observe "print" flag;
2010-07-03 wenzelm 2010-07-03 Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-31 wenzelm 2010-05-31 Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-26 wenzelm 2010-04-26 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 wenzelm 2010-04-23 added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-02-18 wenzelm 2010-02-18 removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
2009-11-17 wenzelm 2009-11-17 init_theory: Runtime.controlled_execution for proper exception trace etc.;
2009-11-17 wenzelm 2009-11-17 implicit name space grouping for theory/local_theory transactions;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 Toplevel.thread provides Isar-style exception output;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Node;
2009-10-27 wenzelm 2009-10-27 non-critical atomic accesses;
2009-09-30 wenzelm 2009-09-30 eliminated dead code; eliminated redundant parameters;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-20 wenzelm 2009-07-20 Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-06-06 wenzelm 2009-06-06 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-04 wenzelm 2009-06-04 exn_message/raised: ML_Compiler.exception_position;
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-21 wenzelm 2009-03-21 restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
2009-03-18 wenzelm 2009-03-18 reduced verbosity;