src/Pure/ML/ml_process.scala
Wed, 25 Jun 2025 12:29:04 +0200 wenzelm clarified signature;
Tue, 24 Jun 2025 22:08:20 +0200 wenzelm clarified modules;
Sun, 15 Jun 2025 22:46:45 +0200 wenzelm more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings;
Sun, 15 Jun 2025 13:13:37 +0200 wenzelm clarified signature: more explicit types;
Sat, 14 Jun 2025 17:10:18 +0200 wenzelm discontinued ML_IDENTIFIER settings variable;
Sat, 14 Jun 2025 14:37:34 +0200 wenzelm clarified modules;
Sat, 14 Jun 2025 14:31:54 +0200 wenzelm clarified signature;
Mon, 01 Jul 2024 12:40:54 +0200 wenzelm clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml;
Sat, 01 Jun 2024 12:35:38 +0200 wenzelm unused;
Sat, 01 Jun 2024 12:31:06 +0200 wenzelm clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
Tue, 16 Apr 2024 16:54:15 +0200 wenzelm clarified signature;
Sun, 18 Feb 2024 19:09:05 +0100 wenzelm clarified signature;
Sat, 17 Feb 2024 21:26:00 +0100 wenzelm more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;
Sat, 17 Feb 2024 21:18:23 +0100 wenzelm tuned names;
Tue, 20 Jun 2023 14:25:06 +0200 wenzelm clarified modules;
Thu, 15 Jun 2023 15:04:23 +0200 wenzelm clarified signature;
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);
Mon, 20 Feb 2023 21:47:25 +0100 wenzelm tuned: avoid redundant white space;
Wed, 21 Dec 2022 13:52:44 +0100 wenzelm clarified signature;
Fri, 16 Dec 2022 18:12:48 +0100 wenzelm clarified signature;
Fri, 16 Dec 2022 17:51:52 +0100 wenzelm clarified names;
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);
less more (0) -50 -30 tip