src/Pure/Thy/thy_info.ML
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;
2007-08-03 wenzelm 2007-08-03 replaced outdated flag by update_time (multithreading-safe presentation order);
2007-08-02 wenzelm 2007-08-02 added int type constraints to accomodate hacked SML/NJ;
2007-07-31 wenzelm 2007-07-31 register_thy: more sanity checks;
2007-07-31 wenzelm 2007-07-31 added register_thy (replaces pretend_use_thy_only and really flag); tuned;
2007-07-30 wenzelm 2007-07-30 marked some CRITICAL sections;
2007-07-29 wenzelm 2007-07-29 deps: keep thy source text, avoid reloading; schedule: pick the first task with maximal imm_succs;
2007-07-29 wenzelm 2007-07-29 removed obsolete Output.ML_errors/toplevel_errors; moved ML toplevel use commands to pure_setup.ML;
2007-07-25 wenzelm 2007-07-25 require_thy/schedule: improved task graph, actually observe dependencies on running tasks;
2007-07-24 wenzelm 2007-07-24 require_thy: tuned tasks graph, removed visited; use_thy etc.: schedule for multithreading;
2007-07-24 wenzelm 2007-07-24 require_thy: explicit tasks graph; added sequential scheduler; internal tuning;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections;
2007-07-22 wenzelm 2007-07-22 added simultaneous use_thys; deps: removed obsolete present'' flag;
2007-07-22 wenzelm 2007-07-22 begin_theory: simplified interface, keep thy info empty until end_theory;
2007-07-21 wenzelm 2007-07-21 deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy); begin_theory: quiet_update_thys in interactive mode, removed no weak_use_thy in batch mode; misc tuning;
2007-07-20 wenzelm 2007-07-20 simplified ThyLoad interfaces: only one additional directory; require_thy: cumulative appending of directory prefix; tuned;
2007-07-19 wenzelm 2007-07-19 removed obsolete use/update_thy_only; removed unused quiet_update_thy, get_succs; renamed get_preds to get_parents; deps: replaced File.info by File.ident (no comparison of paths!); check_deps: reload (partially qualified) parents for unfinished theory, no reference of previously loaded master paths! require_thy: attempt at purely static path lookup, less permissive; misc cleanup;
2007-01-30 aspinall 2007-01-30 Add get_succs
2007-01-21 wenzelm 2007-01-21 *** MESSAGE REFERS TO PREVIOUS VERSION *** @{theory}: plain ML_Context.the_context();
2007-01-21 wenzelm 2007-01-21 tuned comments
2007-01-20 wenzelm 2007-01-20 added @{theory};
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-05-02 wenzelm 2006-05-02 added the_theory;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);