2008-10-01 wenzelm 2008-10-01 removed release_results (cf. Exn.release_all, Exn.release_first);
2008-10-01 wenzelm 2008-10-01 more precise join_futures, improved termination;
2008-10-01 haftmann 2008-10-01 added more_antiquote.ML
2008-10-01 kleing 2008-10-01 extract Isabelle dist name correctly
2008-09-30 wenzelm 2008-09-30 unit_source: explicit treatment of 'oops' proofs;
2008-09-30 wenzelm 2008-09-30 promise_proof: proper statement with empty vars;
2008-09-30 wenzelm 2008-09-30 load_thy: more precise treatment of improper cmd or proof (notably 'oops');
2008-09-30 wenzelm 2008-09-30 schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
2008-09-30 wenzelm 2008-09-30 added unit_source: commands with proof;
2008-09-30 wenzelm 2008-09-30 begin_proof: avoid race condition wrt. skip_proofs flag; replaced command_excursion by excursion, which is based on units of command/proof pairs; excursion: basic support for proof promises;
2008-09-30 wenzelm 2008-09-30 load_thy: Toplevel.excursion based on units of command/proof pairs;
2008-09-30 wenzelm 2008-09-30 more command categories; tuned;
2008-09-30 wenzelm 2008-09-30 renamed Future.fork_irrelevant to Future.fork_background; tuned;
2008-09-30 wenzelm 2008-09-30 export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;
2008-09-30 haftmann 2008-09-30 tuned
2008-09-30 wenzelm 2008-09-30 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
2008-09-30 wenzelm 2008-09-30 Toplevel.commit_exit: position;
2008-09-30 wenzelm 2008-09-30 export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;
2008-09-30 wenzelm 2008-09-30 simplified process_file, eliminated Toplevel.excursion; load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);
2008-09-30 haftmann 2008-09-30 clarified codegen interfaces
2008-09-30 haftmann 2008-09-30 tuned
2008-09-30 haftmann 2008-09-30 reorganized examples
2008-09-30 haftmann 2008-09-30 fixed slips
2008-09-30 haftmann 2008-09-30 re-canibalised manual
2008-09-30 kleing 2008-09-30 slightly different command line for makedist_mercurial
2008-09-29 wenzelm 2008-09-29 put_thms: ContextPosition.set_visible false;
2008-09-29 wenzelm 2008-09-29 added type pp, which helps installing polymorphic pretty printers;
2008-09-29 wenzelm 2008-09-29 added str_of;
2008-09-29 wenzelm 2008-09-29 install_pp Future.T (polyml only);
2008-09-29 wenzelm 2008-09-29 report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29 back to plain Position.report for regular references;
2008-09-29 wenzelm 2008-09-29 back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29 promise global proofs;
2008-09-29 wenzelm 2008-09-29 renamed report to report_visible; tuned comments;
2008-09-29 wenzelm 2008-09-29 code example: back to individual ML commands, which are now thread-safe;
2008-09-29 wenzelm 2008-09-29 ContextPosition.report; parse_token/report_token: explicit context;
2008-09-29 wenzelm 2008-09-29 target update: invisible context position avoids duplication of reports etc.;
2008-09-29 wenzelm 2008-09-29 Context position visibility.
2008-09-29 wenzelm 2008-09-29 added context_position.ML;
2008-09-29 haftmann 2008-09-29 more precise redundancy check
2008-09-29 haftmann 2008-09-29 clarified dependencies between arith tools
2008-09-29 haftmann 2008-09-29 separate HOL-Main image
2008-09-29 haftmann 2008-09-29 polished code generator setup
2008-09-29 haftmann 2008-09-29 added theory antiquotation
2008-09-29 wenzelm 2008-09-29 tuned comments;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-29 wenzelm 2008-09-29 added norm_export_morphism;
2008-09-29 wenzelm 2008-09-29 added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
2008-09-28 wenzelm 2008-09-28 HOL no longer depends on HOL-Plain;
2008-09-28 wenzelm 2008-09-28 setmp_noncritical;
2008-09-28 wenzelm 2008-09-28 join earlier promises first;
2008-09-28 wenzelm 2008-09-28 proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28 wenzelm 2008-09-28 promise_result: enforce strictly sequential dependencies, via serial numbers;
2008-09-28 kleing 2008-09-28 do not cvs update for doc test (switching to mercurial, update done outside once and for all)
2008-09-28 kleing 2008-09-28 use mercurial repository for isatest
2008-09-28 wenzelm 2008-09-28 thread_data: include thread name, export access; more tracing;
2008-09-27 wenzelm 2008-09-27 setmp_noncritical;
2008-09-27 wenzelm 2008-09-27 dequeue_towards: return bound for unfinished tasks;
2008-09-27 wenzelm 2008-09-27 moved release_results to future.ML; get_some: simplified via Future.release_results;