src/Pure/Isar/toplevel.ML
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-02 wenzelm 2013-07-02 clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-05-22 haftmann 2013-05-22 mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
2013-04-23 haftmann 2013-04-23 brittleness stamping for local theories
2013-04-09 wenzelm 2013-04-09 just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09 wenzelm 2013-04-09 clarified protocol_message undefinedness;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-04-03 wenzelm 2013-04-03 more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
2013-04-02 wenzelm 2013-04-02 more centralized command timing; clarified old-style timing message;
2013-03-27 wenzelm 2013-03-27 extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27 wenzelm 2013-03-27 explicit Toplevel.is_skipped_proof; tuned;
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-03-04 wenzelm 2013-03-04 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
2013-03-03 wenzelm 2013-03-03 uniform treatment of global/local proofs; tuned;
2013-03-03 wenzelm 2013-03-03 tuned;
2013-03-03 wenzelm 2013-03-03 clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-03-03 wenzelm 2013-03-03 more Thy_Syntax.element operations;
2013-02-28 wenzelm 2013-02-28 simplified Proof.future_proof;
2013-02-26 wenzelm 2013-02-26 tuned signature;
2013-02-26 wenzelm 2013-02-26 fork diagnostic commands (theory loader and PIDE interaction); explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions; clarified Toplevel.command_exception vs. Toplevel.command_errors;
2013-02-26 wenzelm 2013-02-26 tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;
2013-02-26 wenzelm 2013-02-26 tuned;
2013-02-25 wenzelm 2013-02-25 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2013-02-25 wenzelm 2013-02-25 clarified Toplevel.element_result: scheduling policies happen here; tuned;
2013-02-24 wenzelm 2013-02-24 simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
2013-02-22 wenzelm 2013-02-22 make SML/NJ happy;
2013-02-22 wenzelm 2013-02-22 eliminated hard tabs;
2013-02-21 wenzelm 2013-02-21 highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
2013-02-20 wenzelm 2013-02-20 more tight representation of command timing; tuned signatures; tuned;
2013-02-20 wenzelm 2013-02-20 proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
2013-02-19 wenzelm 2013-02-19 improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-02-19 wenzelm 2013-02-19 suppress timing message in full PIDE protocol -- this is for batch build;
2013-02-19 wenzelm 2013-02-19 support for prescient timing information within command transactions;
2013-02-19 wenzelm 2013-02-19 emit command_timing properties into build log; tuned;
2013-01-16 wenzelm 2013-01-16 tuned signature;
2013-01-05 wenzelm 2013-01-05 more precise Local_Theory.level: 1 really means main target and >= 2 nested context; explicit target for context within global theory with after_close = exit to manage the 2 levels involved here; reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 more precise register_proofs for local goals; tuned signature;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-08-29 wenzelm 2012-08-29 tuned signature;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-11 wenzelm 2012-08-11 vacuous execution after first malformed command;
2012-08-01 wenzelm 2012-08-01 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 wenzelm 2012-05-17 tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
2012-04-11 wenzelm 2012-04-11 clarified proof_result: finish proof formally via head tr, not end_tr;
2012-04-10 wenzelm 2012-04-10 misc tuning and simplification;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-04-02 wenzelm 2012-04-02 misc tuning and simplification;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
2012-03-16 wenzelm 2012-03-16 defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-14 wenzelm 2011-11-14 pass positions for named targets, for formal links in the document model;
2011-08-19 wenzelm 2011-08-19 maintain recent future proofs at transaction boundaries;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;