src/Pure/Isar/toplevel.ML
Wed, 27 Mar 2013 16:38:25 +0100 wenzelm 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);
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Mon, 04 Mar 2013 15:03:46 +0100 wenzelm refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
Sun, 03 Mar 2013 14:29:30 +0100 wenzelm uniform treatment of global/local proofs;
Sun, 03 Mar 2013 13:57:03 +0100 wenzelm tuned;
Sun, 03 Mar 2013 13:43:57 +0100 wenzelm clarified Toplevel.element_result wrt. Toplevel.is_ignored;
Sun, 03 Mar 2013 13:23:06 +0100 wenzelm more Thy_Syntax.element operations;
Thu, 28 Feb 2013 21:11:07 +0100 wenzelm simplified Proof.future_proof;
Tue, 26 Feb 2013 19:58:27 +0100 wenzelm tuned signature;
Tue, 26 Feb 2013 19:44:26 +0100 wenzelm fork diagnostic commands (theory loader and PIDE interaction);
Tue, 26 Feb 2013 13:27:24 +0100 wenzelm tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;
Tue, 26 Feb 2013 11:57:19 +0100 wenzelm tuned;
Mon, 25 Feb 2013 13:29:19 +0100 wenzelm discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
Mon, 25 Feb 2013 12:52:27 +0100 wenzelm clarified Toplevel.element_result: scheduling policies happen here;
Sun, 24 Feb 2013 17:29:55 +0100 wenzelm simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
Fri, 22 Feb 2013 16:52:10 +0100 wenzelm make SML/NJ happy;
Fri, 22 Feb 2013 14:38:52 +0100 wenzelm eliminated hard tabs;
Thu, 21 Feb 2013 10:52:14 +0100 wenzelm highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
Wed, 20 Feb 2013 15:22:22 +0100 wenzelm more tight representation of command timing;
Wed, 20 Feb 2013 11:40:30 +0100 wenzelm proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
Tue, 19 Feb 2013 17:55:26 +0100 wenzelm improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
Tue, 19 Feb 2013 14:47:57 +0100 wenzelm suppress timing message in full PIDE protocol -- this is for batch build;
Tue, 19 Feb 2013 12:58:32 +0100 wenzelm support for prescient timing information within command transactions;
Tue, 19 Feb 2013 10:55:11 +0100 wenzelm emit command_timing properties into build log;
Wed, 16 Jan 2013 21:49:56 +0100 wenzelm tuned signature;
Sat, 05 Jan 2013 17:38:54 +0100 wenzelm more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 16 Oct 2012 15:14:12 +0200 wenzelm more informative errors for 'proof' and 'apply' steps;
Sat, 01 Sep 2012 19:43:18 +0200 wenzelm discontinued complicated/unreliable notion of recent proofs within context;
Fri, 31 Aug 2012 16:35:30 +0200 wenzelm more precise register_proofs for local goals;
Thu, 30 Aug 2012 21:23:04 +0200 wenzelm refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
Thu, 30 Aug 2012 19:18:49 +0200 wenzelm some support for registering forked proofs within Proof.state, using its bottom context;
Thu, 30 Aug 2012 16:39:50 +0200 wenzelm tuned signature;
Wed, 29 Aug 2012 12:07:45 +0200 wenzelm tuned signature;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sat, 11 Aug 2012 19:34:36 +0200 wenzelm vacuous execution after first malformed command;
Wed, 01 Aug 2012 15:33:08 +0200 wenzelm recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
Thu, 17 May 2012 15:23:00 +0200 wenzelm tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
Wed, 11 Apr 2012 15:02:48 +0200 wenzelm clarified proof_result: finish proof formally via head tr, not end_tr;
Tue, 10 Apr 2012 22:53:41 +0200 wenzelm misc tuning and simplification;
Tue, 10 Apr 2012 21:31:05 +0200 wenzelm static relevance of proof via syntax keywords;
Mon, 02 Apr 2012 19:10:52 +0200 wenzelm misc tuning and simplification;
Wed, 21 Mar 2012 23:26:35 +0100 wenzelm more explicit Toplevel.open_target/close_target;
Fri, 16 Mar 2012 14:42:11 +0100 wenzelm defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model;
Fri, 19 Aug 2011 23:25:47 +0200 wenzelm maintain recent future proofs at transaction boundaries;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Mon, 15 Aug 2011 20:38:16 +0200 wenzelm tuned error message;
Sat, 13 Aug 2011 21:06:01 +0200 wenzelm clarified Toplevel.end_theory;
Sat, 13 Aug 2011 20:49:41 +0200 wenzelm simplified Toplevel.init_theory: discontinued special name argument;
Sat, 13 Aug 2011 20:41:29 +0200 wenzelm simplified Toplevel.init_theory: discontinued special master argument;
Sat, 13 Aug 2011 20:20:36 +0200 wenzelm provide node header via Scala layer;
Tue, 05 Jul 2011 20:36:49 +0200 wenzelm get theory from last executation state;
Tue, 05 Jul 2011 19:45:59 +0200 wenzelm explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 26 Mar 2011 21:45:29 +0100 wenzelm present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Fri, 04 Feb 2011 17:11:00 +0100 wenzelm parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
less more (0) -300 -100 -60 tip