| Wed, 30 Sep 2009 23:28:54 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
maintain Future.worker_group as management data;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 19:24:04 +0200 |
wenzelm |
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 11:12:06 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 12:59:16 +0200 |
wenzelm |
schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:47:32 +0100 |
wenzelm |
schedule_seq: handle after_load errors as in schedule_futures;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 23:56:11 +0100 |
wenzelm |
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 16:58:56 +0100 |
wenzelm |
remove_thy: perform PureThy.cancel_proofs;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 13:11:56 +0100 |
wenzelm |
schedule_futures: tuned final consolidation, explicit after_load phase;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 00:25:31 +0100 |
wenzelm |
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 12:13:53 +0100 |
wenzelm |
removed old scheduler;
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 12:14:02 +0100 |
wenzelm |
future proofs: more robust check via Future.enabled;
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:04:44 +0100 |
wenzelm |
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
refined Future.fork interfaces, no longer export Future.future;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:02:46 +0100 |
wenzelm |
future_scheduler: no global task group, exceptions via collective join;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 18:25:59 +0100 |
wenzelm |
force_proofs after cumulative use_thys;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 00:11:06 +0100 |
wenzelm |
finish: force proofs;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2008 20:21:35 +0200 |
wenzelm |
Future.joint_results is already uninterruptible;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 18:16:10 +0200 |
wenzelm |
future_schedule: back to one group for all loader tasks;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:05 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 22:02:55 +0200 |
wenzelm |
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:21 +0200 |
wenzelm |
moved future_scheduler flag to skip_proof.ML;
|
file |
diff |
annotate
|
| Fri, 19 Sep 2008 21:22:31 +0200 |
wenzelm |
future tasks: support boolean priorities (true = high, false = low/irrelevant);
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:49 +0200 |
wenzelm |
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 22:29:36 +0200 |
wenzelm |
future_schedule: uninterruptible join;
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 21:50:32 +0200 |
wenzelm |
added future_scheduler (default false);
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:49 +0200 |
wenzelm |
moved Multithreading.task/schedule to Concurrent/schedule.ML
|
file |
diff |
annotate
|
| Tue, 12 Aug 2008 21:28:05 +0200 |
wenzelm |
load_thy: removed obsolete dir argument;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:51:48 +0200 |
wenzelm |
end_theory: no result;
|
file |
diff |
annotate
|
| Tue, 08 Jul 2008 17:52:28 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:21 +0200 |
wenzelm |
moved concrete antiquotations to ml_antiquote.ML;
|
file |
diff |
annotate
|
| Sat, 24 May 2008 20:12:17 +0200 |
wenzelm |
exported master_directory;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 11:05:08 +0200 |
wenzelm |
renamed Position.path to Path.position;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2008 14:53:30 +0200 |
wenzelm |
export get_names (formerly names);
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:16 +0100 |
wenzelm |
added exec_file;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
| Sun, 27 Jan 2008 22:21:37 +0100 |
wenzelm |
use_thy: do not set implicit ML context anymore;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 16:32:53 +0100 |
wenzelm |
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 21:12:03 +0100 |
wenzelm |
scheduling/next_task: PrintMode.closure;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 16:13:46 +0200 |
wenzelm |
require_thy: read_text *after* checking parents
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 21:37:00 +0200 |
wenzelm |
added generic provide_file;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 21:07:41 +0200 |
wenzelm |
added @{theory_ref};
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:39 +0200 |
wenzelm |
export is_finished;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:46 +0200 |
wenzelm |
removed obsolete touch_all_thys;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 17:49:33 +0200 |
wenzelm |
check_deps: ensure that theory is actually present, not just update_time > 1;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 14:14:24 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2007 17:50:23 +0200 |
wenzelm |
schedule_tasks: alphabetical order for equivalent tasks;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 23:53:51 +0200 |
wenzelm |
schedule: misc cleanup, more precise task model;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 23:07:50 +0200 |
wenzelm |
discontinued attached ML files;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 20:48:08 +0200 |
wenzelm |
check_deps: really do reload the master text if required;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:51 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 22:33:10 +0200 |
wenzelm |
replaced outdated flag by update_time (multithreading-safe presentation order);
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 21:45:07 +0200 |
wenzelm |
added int type constraints to accomodate hacked SML/NJ;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:28 +0200 |
wenzelm |
register_thy: more sanity checks;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:34 +0200 |
wenzelm |
added register_thy (replaces pretend_use_thy_only and really flag);
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 22:42:02 +0200 |
wenzelm |
deps: keep thy source text, avoid reloading;
|
file |
diff |
annotate
|