| 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);
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 14:47:57 +0100 |
wenzelm |
suppress timing message in full PIDE protocol -- this is for batch build;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 12:58:32 +0100 |
wenzelm |
support for prescient timing information within command transactions;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 10:55:11 +0100 |
wenzelm |
emit command_timing properties into build log;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 21:49:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 17:38:54 +0100 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:43:18 +0200 |
wenzelm |
discontinued complicated/unreliable notion of recent proofs within context;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 16:35:30 +0200 |
wenzelm |
more precise register_proofs for local goals;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
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 |
wenzelm |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 16:39:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 12:07:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 19:34:36 +0200 |
wenzelm |
vacuous execution after first malformed command;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 11 Apr 2012 15:02:48 +0200 |
wenzelm |
clarified proof_result: finish proof formally via head tr, not end_tr;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 22:53:41 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 21:31:05 +0200 |
wenzelm |
static relevance of proof via syntax keywords;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 19:10:52 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 23:26:35 +0100 |
wenzelm |
more explicit Toplevel.open_target/close_target;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 23:25:47 +0200 |
wenzelm |
maintain recent future proofs at transaction boundaries;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 17:53:32 +0200 |
wenzelm |
more careful treatment of exception serial numbers, with propagation to message channel;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 20:38:16 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 21:06:01 +0200 |
wenzelm |
clarified Toplevel.end_theory;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 20:36:49 +0200 |
wenzelm |
get theory from last executation state;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 11:16:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Fri, 04 Feb 2011 17:11:00 +0100 |
wenzelm |
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 23:02:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
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 |
wenzelm |
formal notepad without any result;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
avoid extra wrapping for interrupts;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 18:18:34 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:20:27 +0200 |
wenzelm |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:46:49 +0200 |
wenzelm |
moved Toplevel.run_command to Pure/PIDE/document.ML;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:49:41 +0200 |
wenzelm |
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:19:39 +0200 |
wenzelm |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 21:31:22 +0200 |
wenzelm |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:42:13 +0200 |
haftmann |
named target is optional; explicit Name_Target.reinit
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 20:25:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:16:02 +0200 |
haftmann |
avoid arcane Local_Theory.reinit entirely
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 18:17:53 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|