src/Pure/System/bash.scala
Thu, 22 Apr 2021 23:40:22 +0200 wenzelm fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
Thu, 22 Apr 2021 23:03:58 +0200 wenzelm clarified signature;
Thu, 22 Apr 2021 22:07:05 +0200 wenzelm clarified command-line;
Mon, 12 Apr 2021 18:10:13 +0200 wenzelm clarified signature for Scala functions;
Sat, 13 Mar 2021 12:36:24 +0100 wenzelm clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
Thu, 04 Mar 2021 21:04:27 +0100 wenzelm clarified signature --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 18:11:06 +0100 wenzelm clarified signature;
Mon, 22 Feb 2021 12:30:05 +0100 wenzelm clarified signature: process_result timing from Isabelle/Scala;
Sun, 21 Feb 2021 13:14:08 +0100 wenzelm more accurate process_result in ML, corresponding to Process_Result in Scala;
Sun, 21 Feb 2021 00:49:09 +0100 wenzelm clarified lines (again);
Sat, 20 Feb 2021 22:09:16 +0100 wenzelm more uniform Bash.process: always ask Isabelle/Scala;
Sun, 07 Feb 2021 20:39:15 +0100 wenzelm more robust: allow YXML text;
Sun, 07 Feb 2021 16:31:43 +0100 wenzelm support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
Sat, 16 Jan 2021 17:02:14 +0100 wenzelm clarified return code: re-use SIGALRM for soft timeout;
Thu, 12 Nov 2020 16:07:25 +0100 wenzelm support for watchdog thread;
Thu, 06 Aug 2020 22:58:18 +0200 wenzelm unused --- superseded by PIDE messages;
Mon, 06 Apr 2020 21:04:33 +0200 wenzelm more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
Mon, 06 Apr 2020 14:03:58 +0200 wenzelm terminate faster;
Mon, 06 Apr 2020 13:59:48 +0200 wenzelm tuned;
Mon, 06 Apr 2020 13:54:45 +0200 wenzelm tuned;
Mon, 06 Apr 2020 13:40:44 +0200 wenzelm clarified interrupt handling;
Sat, 04 Apr 2020 18:13:05 +0200 wenzelm clarified signature;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Thu, 14 Dec 2017 14:27:37 +0100 wenzelm tuned;
Sat, 18 Mar 2017 22:11:05 +0100 wenzelm more informative session result;
Sat, 18 Mar 2017 21:40:47 +0100 wenzelm simplified signature (despite 448325de6e4f);
Mon, 16 Jan 2017 15:50:54 +0100 wenzelm tuned -- nicer generated bash source;
Tue, 18 Oct 2016 16:03:30 +0200 wenzelm clarified modules;
Sun, 02 Oct 2016 19:36:57 +0200 wenzelm tuned whitespace;
Mon, 05 Sep 2016 22:09:52 +0200 wenzelm clarified modules;
Sun, 13 Mar 2016 12:37:01 +0100 wenzelm more uniform signature for various process invocations;
Sat, 12 Mar 2016 22:11:09 +0100 wenzelm tuned;
Sat, 12 Mar 2016 21:46:31 +0100 wenzelm more thorough cleanup -- in Scala;
Thu, 10 Mar 2016 09:50:53 +0100 wenzelm clarified files;
less more (0) tip