| Fri, 12 Oct 2012 13:55:13 +0200 |
wenzelm |
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 13:46:41 +0200 |
wenzelm |
do not treat interrupt as error here, to avoid confusion in log etc.;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:27:28 +0200 |
wenzelm |
central management of forked goals wrt. transaction id;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 15:25:26 +0200 |
wenzelm |
more informative error message from failed goal forks (violating old-style TTY protocol!);
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 14:35:04 +0200 |
wenzelm |
more markup for failed goal forks, reusing "bad";
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 13:23:25 +0200 |
wenzelm |
further refinement of command status, to accomodate forked proofs;
|
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 15:26:37 +0200 |
wenzelm |
refined status of forked goals;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 20:42:17 +0200 |
wenzelm |
tuned future priorities: print 0, goal ~1, execute ~2;
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 16:25:32 +0100 |
wenzelm |
depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:24:39 +0200 |
wenzelm |
Goal.forked: clarified handling of interrupts;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 23:38:25 +0200 |
wenzelm |
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 22:21:34 +0200 |
wenzelm |
refined PARALLEL_GOALS;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Tue, 22 Feb 2011 19:44:15 +0100 |
wenzelm |
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 16:11:58 +0100 |
wenzelm |
less verbose tracing;
|
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
|
| Wed, 02 Feb 2011 15:04:09 +0100 |
wenzelm |
maintain Task_Queue.group within Task_Queue.task;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 23:53:07 +0100 |
wenzelm |
more specific Goal.fork_name;
|
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
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 21:13:53 +0200 |
wenzelm |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
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
|
| Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|