src/Pure/goal.ML
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 ago more basic Goal.reset_futures as snapshot of implicit state;
2012-10-17 ago more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
2012-10-13 ago some attempts to unify/simplify pretty_goal;
2012-10-13 ago tuned signature;
2012-10-12 ago no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
2012-10-12 ago do not treat interrupt as error here, to avoid confusion in log etc.;
2012-09-01 ago central management of forked goals wrt. transaction id;
2012-08-31 ago more informative error message from failed goal forks (violating old-style TTY protocol!);
2012-08-31 ago more markup for failed goal forks, reusing "bad";
2012-08-31 ago further refinement of command status, to accomodate forked proofs;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30 ago refined status of forked goals;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-04-10 ago tuned future priorities: print 0, goal ~1, execute ~2;
2011-11-11 ago depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
2011-11-05 ago added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
2011-08-19 ago tuned;
2011-08-10 ago Goal.forked: clarified handling of interrupts;
2011-08-10 ago future_job: explicit indication of interrupts;
2011-04-27 ago clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-16 ago enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
2011-04-16 ago refined PARALLEL_GOALS;
2011-04-16 ago modernized structure Proof_Context;
2011-02-22 ago scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
2011-02-18 ago less verbose tracing;
2011-02-04 ago parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2011-02-02 ago maintain Task_Queue.group within Task_Queue.task;
2011-01-31 ago more specific Goal.fork_name;
2011-01-31 ago tuned signature;
2011-01-31 ago support named tasks, for improved tracing;
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-03 ago 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;
2010-08-30 ago tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-06 ago removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-07-04 ago general Future.report -- also for Toplevel.async_state;
2010-05-29 ago explicit markup for forked goals, as indicated by Goal.fork;
2010-05-03 ago simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-19 ago future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
2009-09-30 ago PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-12 ago added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-07-28 ago eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-26 ago Goal.finish: explicit context for printing;
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-07-20 ago Proof.future_proof: declare all assumptions as well;
2009-07-19 ago parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 ago more abstract Future.is_worker;
2009-07-19 ago future_result: explicitly impose Variable.sorts_of again;
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-01-11 ago added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-10 ago added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-04 ago tuned protect, conclude: Drule.comp_no_flatten;
2009-01-04 ago future proofs: back to Future.fork_pri ~1 for improved parallelism;