src/Pure/Isar/toplevel.ML
2 months ago ago tuned;
2 months ago ago tuned -- more explicit type node_presentation;
2 months ago ago tuned signature;
3 months ago ago Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;
3 months ago ago keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);
4 months ago ago Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
8 months ago ago clarified reset_notepad;
8 months ago ago more robust reset_state: begin/end structure takes precedence over goal/proof structure;
8 months ago ago no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
8 months ago ago clarified signature;
8 months ago ago clarified message;
8 months ago ago clarified modules;
9 months ago ago tuned
10 months ago ago clarified default tag;
12 months ago ago clarified future scheduling parameters, with support for parallel_limit;
14 months ago ago clarified signature;
15 months ago ago clarified apply_transaction: always continue without presentation context;
15 months ago ago more tight presentation context: avoid storing full Toplevel.state;
15 months ago ago tuned;
16 months ago ago tuned;
16 months ago ago clarified signature;
16 months ago ago clarified presentation_state with provide presentation_context;
16 months ago ago theory Pure is default presentation context;
16 months ago ago more operations;
17 months ago ago uniform use of original theory;
17 months ago ago clarified document preparation vs. skip_proofs;
23 months ago ago keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
24 months ago ago clarified build errors;
2017-02-27 ago clarified priority: zero can mean unknown/long or irrelevant/short time;
2017-02-27 ago absent timing information means zero, according to 0070053570c4, f235646b1b73;
2017-02-26 ago tuned;
2016-04-06 ago treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-06 ago clarified modules;
2016-04-02 ago prefer infix operations;
2016-04-02 ago careful export of type-dependent functions, without losing their special status;
2016-03-18 ago clarified modules;
2016-03-03 ago clarified modules;
2016-01-24 ago tuned;
2015-12-21 ago discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-09-21 ago separate panel for proof state output;
2015-08-11 ago default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-08 ago more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-06-09 ago tuned signature;
2015-05-03 ago tuned output;
2015-04-22 ago allow diagnostic proof commands with skip_proofs;
2015-04-22 ago tuned signature;
2015-04-16 ago discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 ago explicit error for Toplevel.proof_of;
2015-04-15 ago tuned messages;
2015-04-09 ago clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 ago support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 ago support private scope for individual local theory commands;
2015-01-29 ago 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 ago explicit message channels for "state", "information";
2014-12-19 ago tuned;
2014-11-26 ago more informative failure of protocol commands, with exception trace;
2014-11-22 ago tuned;
2014-11-13 ago uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
2014-11-06 ago more explicit Keyword.keywords;
2014-11-03 ago eliminated unused int_only flag (see also c12484a27367);