src/Pure/Thy/thy_info.ML
2010-07-21 wenzelm 2010-07-21 replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-01-05 wenzelm 2010-01-05 kill failed theories in reverse order -- avoids cascaded warnings;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-01 wenzelm 2009-10-01 added Task_Queue.depend (again) -- light-weight version for transitive graph; Future.join_results: record explicit dependency, detect direct task-task join cycles; Future.join_results: no change of interruptibility, allows to interrupt wait; added Future.worker_task; ThyInfo.schedule_futures: uninterruptible outer join;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings; schedule_tasks/require_thy: eliminated obsolete tasks_len, which was a leftover from theory-only parallelization;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-21 wenzelm 2009-07-21 maintain Future.worker_group as management data; cancel_thy: refer to proper task group; tuned;
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-06-10 wenzelm 2009-06-10 reraise exceptions to preserve position information;
2009-03-31 wenzelm 2009-03-31 schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
2009-03-06 wenzelm 2009-03-06 schedule_seq: handle after_load errors as in schedule_futures;
2009-01-10 wenzelm 2009-01-10 schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10 wenzelm 2009-01-10 remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;
2009-01-10 wenzelm 2009-01-10 schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10 wenzelm 2009-01-10 use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2008-12-16 wenzelm 2008-12-16 removed old scheduler;
2008-12-12 wenzelm 2008-12-12 future proofs: more robust check via Future.enabled;
2008-12-06 wenzelm 2008-12-06 improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
2008-12-04 wenzelm 2008-12-04 refined Future.fork interfaces, no longer export Future.future;
2008-12-04 wenzelm 2008-12-04 future_scheduler: no global task group, exceptions via collective join; finish: removed PureThy.force_proofs, back to old version;
2008-11-18 wenzelm 2008-11-18 force_proofs after cumulative use_thys; PureThy.force_proofs;
2008-11-18 wenzelm 2008-11-18 finish: force proofs;
2008-10-08 wenzelm 2008-10-08 Future.joint_results is already uninterruptible;
2008-10-01 wenzelm 2008-10-01 future_schedule: back to one group for all loader tasks;
2008-10-01 wenzelm 2008-10-01 more robust treatment of Interrupt (cf. exn.ML); future_schedule: group each theory separately;
2008-09-30 wenzelm 2008-09-30 schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
2008-09-25 wenzelm 2008-09-25 moved future_scheduler flag to skip_proof.ML;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-18 wenzelm 2008-09-18 begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
2008-09-10 wenzelm 2008-09-10 future_schedule: uninterruptible join;
2008-09-10 wenzelm 2008-09-10 added future_scheduler (default false);
2008-09-04 wenzelm 2008-09-04 moved Multithreading.task/schedule to Concurrent/schedule.ML
2008-08-12 wenzelm 2008-08-12 load_thy: removed obsolete dir argument;
2008-07-14 wenzelm 2008-07-14 end_theory: no result;
2008-07-08 wenzelm 2008-07-08 moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; non-pervasive touch_thy, remove_thy;
2008-06-24 wenzelm 2008-06-24 moved concrete antiquotations to ml_antiquote.ML;
2008-05-24 wenzelm 2008-05-24 exported master_directory;
2008-05-14 wenzelm 2008-05-14 renamed Position.path to Path.position;
2008-04-10 wenzelm 2008-04-10 export get_names (formerly names); moved pervasive theory = ThyInfo.get_theory to pure_setup.ML; removed unused pretty_theory; use OuterSyntax.load_thy instead of backpatched ThyLoad.load_thy;
2008-03-29 wenzelm 2008-03-29 added exec_file; tuned;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-01-27 wenzelm 2008-01-27 use_thy: do not set implicit ML context anymore;
2008-01-02 wenzelm 2008-01-02 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
2007-12-20 wenzelm 2007-12-20 scheduling/next_task: PrintMode.closure;
2007-10-14 wenzelm 2007-10-14 require_thy: read_text *after* checking parents (otherwise outdating an existing descendant will leave the dependencies corrupted);
2007-10-12 wenzelm 2007-10-12 added generic provide_file; tuned;
2007-09-24 wenzelm 2007-09-24 added @{theory_ref};
2007-09-08 wenzelm 2007-09-08 export is_finished; added thy_ord (based on update_time); begin_thy/register_thy: more precise handling of update_time;
2007-08-17 wenzelm 2007-08-17 removed obsolete touch_all_thys;
2007-08-17 wenzelm 2007-08-17 check_deps: ensure that theory is actually present, not just update_time > 1;
2007-08-12 wenzelm 2007-08-12 made SML/NJ happy;
2007-08-11 wenzelm 2007-08-11 schedule_tasks: alphabetical order for equivalent tasks;
2007-08-09 wenzelm 2007-08-09 schedule: misc cleanup, more precise task model;
2007-08-08 wenzelm 2007-08-08 discontinued attached ML files; end_theory: fail on unresolved dependencies;
2007-08-08 wenzelm 2007-08-08 check_deps: really do reload the master text if required; load_thy: more robust check of corrupted deps; require_thy: outdate_thy if required; tuned;
2007-08-07 wenzelm 2007-08-07 theory loader: removed obsolete update_thy (coincides with use_thy); tuned; tuned comments;