src/Pure/Tools/build_job.scala
Wed, 25 Nov 2020 12:52:00 +0100 wenzelm clarified document_output vs. progress;
Tue, 24 Nov 2020 16:49:42 +0100 wenzelm more robust;
Tue, 24 Nov 2020 16:39:58 +0100 wenzelm clarified signature and database layout;
Mon, 23 Nov 2020 15:34:35 +0100 wenzelm unused;
Mon, 23 Nov 2020 15:14:58 +0100 wenzelm support for PIDE markup in batch build (inactive due to pide_reports=false);
Sat, 21 Nov 2020 21:02:38 +0100 wenzelm clarified signature: prefer Database_Context;
Sat, 21 Nov 2020 17:12:17 +0100 wenzelm clarified document output;
Sat, 21 Nov 2020 16:07:20 +0100 wenzelm clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
Thu, 19 Nov 2020 21:23:12 +0100 wenzelm clarified signature;
Thu, 19 Nov 2020 21:12:35 +0100 wenzelm clarified modules;
less more (0) tip