src/Pure/ML/ml_process.scala
Tue, 14 Mar 2023 10:35:41 +0100 wenzelm clarified modules;
Thu, 02 Mar 2023 16:09:22 +0100 wenzelm clarified names;
Thu, 02 Mar 2023 15:55:20 +0100 wenzelm tuned, following ML_Statistics.monitor;
Thu, 02 Mar 2023 15:39:21 +0100 wenzelm tuned;
Tue, 28 Feb 2023 17:42:13 +0100 wenzelm clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
Tue, 28 Feb 2023 17:16:50 +0100 wenzelm tuned;
Tue, 28 Feb 2023 17:12:39 +0100 wenzelm simplified somewhat pointless error message (see also 0189fe0f6452);
less more (0) -30 -10 -7 tip