src/Pure/ML/ml_process.scala
Fri, 16 Dec 2022 17:30:29 +0100 wenzelm clarified signature;
Fri, 16 Dec 2022 17:02:10 +0100 wenzelm tuned signature;
Sat, 20 Aug 2022 13:28:31 +0200 wenzelm clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
Wed, 17 Aug 2022 15:18:17 +0200 wenzelm clarified signature: avoid constants from Sessions.Structure within Session.Base;
less more (0) -30 -10 -4 tip