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