2015-01-10 wenzelm [Sat, 10 Jan 2015 11:48:52 +0100] rev 59337
tuned;
src/Pure/Concurrent/event_timer.ML

2015-01-10 nipkow [Sat, 10 Jan 2015 13:31:37 +0100] rev 59336
added lemma
src/HOL/Finite_Set.thy

2015-01-10 haftmann [Sat, 10 Jan 2015 10:40:11 +0100] rev 59335
typo
src/Doc/Codegen/Evaluation.thy

2015-01-10 haftmann [Sat, 10 Jan 2015 10:24:30 +0100] rev 59334
avoid writing into source
src/Doc/Codegen/Evaluation.thy src/Doc/Codegen/Introduction.thy src/Doc/Codegen/Setup.thy src/Doc/Codegen/document/build

2015-01-09 wenzelm [Fri, 09 Jan 2015 21:20:07 +0100] rev 59333
clarified active_job: take dependencies into account (e.g. future based on promise);
src/Pure/Concurrent/task_queue.ML

2015-01-09 wenzelm [Fri, 09 Jan 2015 20:51:26 +0100] rev 59332
tuned;
src/Pure/Concurrent/task_queue.ML

2015-01-09 wenzelm [Fri, 09 Jan 2015 20:39:17 +0100] rev 59331
non-strict print_state: display old proof state on failure, e.g. unfinished command;
src/Pure/PIDE/command.ML

2015-01-09 wenzelm [Fri, 09 Jan 2015 20:12:42 +0100] rev 59330
permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
src/Pure/Concurrent/future.ML

2015-01-09 wenzelm [Fri, 09 Jan 2015 19:20:00 +0100] rev 59329
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;
src/Pure/Concurrent/event_timer.ML

2015-01-09 wenzelm [Fri, 09 Jan 2015 11:51:02 +0100] rev 59328
ignore print process even after fork, to avoid loosing active worker threads;
src/Pure/PIDE/command.ML