src/Pure/Isar/toplevel.ML
10 months ago wenzelm 2017-12-07 clarified document preparation vs. skip_proofs;
16 months ago wenzelm 2017-06-22 keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
16 months ago wenzelm 2017-05-27 clarified build errors; tuned signature;
19 months ago wenzelm 2017-02-27 clarified priority: zero can mean unknown/long or irrelevant/short time;
19 months ago wenzelm 2017-02-27 absent timing information means zero, according to 0070053570c4, f235646b1b73;
19 months ago wenzelm 2017-02-26 tuned;
2016-04-06 wenzelm 2016-04-06 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2016-01-24 wenzelm 2016-01-24 tuned;
2015-12-21 wenzelm 2015-12-21 discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-09-21 wenzelm 2015-09-21 separate panel for proof state output;
2015-08-11 wenzelm 2015-08-11 default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-08 wenzelm 2015-07-08 more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-22 wenzelm 2015-04-22 tuned signature;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-15 wenzelm 2015-04-15 tuned messages;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 support private scope for individual local theory commands; tuned signature;
2015-01-29 wenzelm 2015-01-29 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-11-26 wenzelm 2014-11-26 more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
2014-11-22 wenzelm 2014-11-22 tuned;
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-31 wenzelm 2014-10-31 discontinued pointless option: timing is always on (overall theory only);
2014-10-31 wenzelm 2014-10-31 eliminated odd flags and hook;
2014-10-28 wenzelm 2014-10-28 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28 wenzelm 2014-10-28 tuned;
2014-07-02 haftmann 2014-07-02 centralized (ad-hoc) switching of targets in named_target.ML
2014-06-07 haftmann 2014-06-07 avoid odd Named_Target.reinit altogether
2014-06-07 haftmann 2014-06-07 clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-05-12 wenzelm 2014-05-12 smarter recovery from toplevel type error;
2014-05-07 wenzelm 2014-05-07 print results as "state", to avoid intrusion into the source text; print new local theory (again);
2014-05-07 wenzelm 2014-05-07 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-07 wenzelm 2014-05-07 tuned;
2014-05-06 wenzelm 2014-05-06 clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-05 wenzelm 2014-05-05 more print operations; preserve declaration order;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-24 wenzelm 2014-03-24 discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-14 wenzelm 2014-03-14 prefer more robust Synchronized.var;
2014-03-12 wenzelm 2014-03-12 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
2014-03-11 wenzelm 2014-03-11 slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;
2014-02-13 wenzelm 2014-02-13 tuned whitespace;
2013-12-05 wenzelm 2013-12-05 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash; tuned signature;
2013-11-11 wenzelm 2013-11-11 tuned signature;
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;