Mon, 15 Sep 2008 16:43:53 +0200 wenzelm tuned comment;
Mon, 15 Sep 2008 16:43:31 +0200 wenzelm added formal markup for setting, executable, tool;
Mon, 15 Sep 2008 16:42:09 +0200 wenzelm basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
Mon, 15 Sep 2008 16:42:00 +0200 wenzelm converted basics.tex to theory file;
Mon, 15 Sep 2008 16:40:53 +0200 wenzelm added isatt markup;
Sun, 14 Sep 2008 21:50:35 +0200 haftmann New outline for codegen tutorial -- draft
Fri, 12 Sep 2008 12:04:20 +0200 wenzelm added extern_fact (local or global);
Fri, 12 Sep 2008 12:04:19 +0200 wenzelm print raw (internal) result names;
Fri, 12 Sep 2008 12:04:16 +0200 wenzelm more procise printing of fact names;
Fri, 12 Sep 2008 10:54:00 +0200 wenzelm pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
Thu, 11 Sep 2008 22:22:59 +0200 wenzelm cancel, shutdown: notify_all;
Thu, 11 Sep 2008 22:22:20 +0200 wenzelm finish: Future.shutdown last;
Thu, 11 Sep 2008 21:53:53 +0200 wenzelm eliminated requests, use global state variables uniformly;
Thu, 11 Sep 2008 21:04:09 +0200 wenzelm finish: Future.shutdown;
Thu, 11 Sep 2008 21:04:07 +0200 wenzelm added is_empty;
Thu, 11 Sep 2008 21:04:05 +0200 wenzelm shutdown: global join-and-shutdown operation;
Thu, 11 Sep 2008 18:07:58 +0200 wenzelm added focus, which indicates a particular collection of high-priority tasks;
Thu, 11 Sep 2008 13:43:42 +0200 wenzelm some general notes on future values;
Thu, 11 Sep 2008 13:24:19 +0200 wenzelm separate Concurrent/ROOT.ML;
Thu, 11 Sep 2008 13:24:14 +0200 wenzelm Parallel list combinators.
Thu, 11 Sep 2008 13:23:57 +0200 wenzelm added Concurrent/par_list.ML;
Wed, 10 Sep 2008 23:28:09 +0200 wenzelm added interrupt_task (external id);
Wed, 10 Sep 2008 23:19:36 +0200 wenzelm tuned;
Wed, 10 Sep 2008 22:29:36 +0200 wenzelm future_schedule: uninterruptible join;
Wed, 10 Sep 2008 21:50:32 +0200 wenzelm added future_scheduler (default false);
Wed, 10 Sep 2008 21:50:30 +0200 wenzelm replaced join_all by join_results, which returns Exn.results;
Wed, 10 Sep 2008 20:28:01 +0200 wenzelm workers: explicit activity flag;
Wed, 10 Sep 2008 19:44:29 +0200 wenzelm future: allow explicit group;
Wed, 10 Sep 2008 19:44:28 +0200 wenzelm cancel: invalidate group implicitly, via bool ref;
Wed, 10 Sep 2008 11:36:37 +0200 wenzelm auto_flush: uniform block buffering for all output streams;
Tue, 09 Sep 2008 23:48:38 +0200 wenzelm auto_flush stdout, stderr as well;
Tue, 09 Sep 2008 23:48:36 +0200 wenzelm proper values of no_interrupts, regular_interrupts;
Tue, 09 Sep 2008 23:30:05 +0200 wenzelm cancel: check_scheduler;
Tue, 09 Sep 2008 23:30:00 +0200 wenzelm simplified dequeue: provide Thread.self internally;
Tue, 09 Sep 2008 20:22:40 +0200 wenzelm eliminated cache, access queue efficiently via IntGraph.get_first;
Tue, 09 Sep 2008 20:22:30 +0200 wenzelm export get_first from underlying table;
Tue, 09 Sep 2008 19:57:54 +0200 wenzelm out_stream: block-buffered, with separate autoflush thread (every 50ms);
Tue, 09 Sep 2008 19:36:21 +0200 wenzelm babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
Tue, 09 Sep 2008 19:33:22 +0200 nipkow added comment
Tue, 09 Sep 2008 16:59:48 +0200 wenzelm human-readable printing of TaskQueue.task/group;
Tue, 09 Sep 2008 16:35:57 +0200 wenzelm * Changed defaults for unify configuration options;
Tue, 09 Sep 2008 16:29:34 +0200 wenzelm inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
Tue, 09 Sep 2008 16:29:32 +0200 wenzelm job: explicit 'ok' status -- false for canceled jobs;
Tue, 09 Sep 2008 16:17:08 +0200 paulson Overall exception handler in order to insulate our users from low-level bugs.
Tue, 09 Sep 2008 16:16:20 +0200 paulson more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
Tue, 09 Sep 2008 16:15:25 +0200 paulson Increasing the default limits in order to prevent unnecessary failures.
Mon, 08 Sep 2008 22:14:39 +0200 wenzelm send: broadcast condition while locked!
Mon, 08 Sep 2008 21:08:30 +0200 wenzelm proper signature constraint;
Mon, 08 Sep 2008 20:35:38 +0200 wenzelm tuned Mailbox.send;
Mon, 08 Sep 2008 20:33:29 +0200 wenzelm removed unused sync_interrupts;
Mon, 08 Sep 2008 20:33:27 +0200 wenzelm moved thread data to future.ML (again);
Mon, 08 Sep 2008 20:33:24 +0200 wenzelm more interrupt operations;
Mon, 08 Sep 2008 16:08:23 +0200 wenzelm moved task, thread_data, group, queue to task_queue.ML;
Mon, 08 Sep 2008 16:08:18 +0200 wenzelm Ordered queue of grouped tasks.
Mon, 08 Sep 2008 16:08:13 +0200 wenzelm added Concurrent/task_queue.ML;
Mon, 08 Sep 2008 00:25:34 +0200 wenzelm await: SYNCHRONIZED wait!
Mon, 08 Sep 2008 00:10:41 +0200 wenzelm tuned check_cache;
Sun, 07 Sep 2008 22:20:15 +0200 wenzelm added sync_interrupts, regular_interrupts;
Sun, 07 Sep 2008 22:20:11 +0200 wenzelm added sync_interrupts, regular_interrupts;
Sun, 07 Sep 2008 22:20:08 +0200 wenzelm opaque signature constraint abstracts local type abbrev;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip