src/Pure/System/isabelle_process.scala
Sat, 14 Jun 2025 14:31:54 +0200 wenzelm clarified signature;
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;
Fri, 24 Nov 2023 20:58:12 +0100 wenzelm disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);
Fri, 24 Nov 2023 16:17:29 +0100 wenzelm prefer Unix-domain socket on Unix;
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;
Fri, 24 Feb 2023 20:40:50 +0100 wenzelm tuned;
Wed, 21 Dec 2022 13:52:44 +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;
Wed, 09 Nov 2022 12:32:20 +0100 wenzelm clarified signature: more public operations;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Wed, 30 Jun 2021 11:35:07 +0200 wenzelm clarified signature: prefer Java interfaces;
Fri, 04 Jun 2021 22:50:32 +0200 wenzelm tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);
Fri, 04 Jun 2021 22:46:11 +0200 wenzelm clarified signature;
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;
Sat, 02 Jan 2021 22:22:34 +0100 wenzelm clarified signature: absorb XZ.Cache into XML.Cache;
Mon, 06 Apr 2020 22:28:41 +0200 wenzelm more robust interrupts;
Thu, 02 Apr 2020 20:06:43 +0200 wenzelm proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
Tue, 31 Mar 2020 22:27:02 +0200 wenzelm clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
Sat, 28 Mar 2020 14:01:45 +0100 wenzelm clarified Isabelle_Process phases;
Sat, 28 Mar 2020 13:30:38 +0100 wenzelm tuned error message;
Sat, 28 Mar 2020 12:06:37 +0100 wenzelm clarified signature: more robust startup_join;
Fri, 27 Mar 2020 12:46:56 +0100 wenzelm clarified signature;
Fri, 27 Mar 2020 12:28:55 +0100 wenzelm clarified signature;
Fri, 27 Mar 2020 12:03:20 +0100 wenzelm clarified signature;
Wed, 02 Jan 2019 20:20:01 +0100 wenzelm more robust system channel via options that are private to the user;
Fri, 18 May 2018 17:09:55 +0200 wenzelm support Store with options;
Thu, 17 May 2018 15:38:36 +0200 wenzelm clarified signature;
Sun, 13 May 2018 16:37:36 +0200 wenzelm tuned signature;
Sun, 10 Dec 2017 20:29:00 +0100 wenzelm avoid println with its extra CR on Windows;
Sun, 12 Nov 2017 12:41:05 +0100 wenzelm tuned signature;
Thu, 06 Apr 2017 22:04:30 +0200 wenzelm clarified signature: tree structure is not essential;
Sat, 01 Apr 2017 22:03:24 +0200 wenzelm clarified YXML vs. symbol encoding: operate on whole message;
Sat, 18 Mar 2017 21:40:47 +0100 wenzelm simplified signature (despite 448325de6e4f);
Sat, 18 Mar 2017 20:24:12 +0100 wenzelm more process arguments;
Tue, 14 Mar 2017 11:48:15 +0100 wenzelm support for permanent phase_changed watcher;
Mon, 13 Mar 2017 23:24:20 +0100 wenzelm more explicit Session.xml_cache;
Mon, 13 Mar 2017 22:50:26 +0100 wenzelm tuned signature;
Tue, 29 Mar 2016 23:41:28 +0200 wenzelm proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
Fri, 18 Mar 2016 17:58:19 +0100 wenzelm discontinued slightly odd "secure" mode;
Wed, 16 Mar 2016 11:45:25 +0100 wenzelm less physical "logic" argument, with option -l like "isabelle console" etc.;
Tue, 15 Mar 2016 23:59:39 +0100 wenzelm find heaps uniformly via Sessions.Store;
Thu, 10 Mar 2016 10:07:23 +0100 wenzelm clarified modules;
Tue, 08 Mar 2016 20:33:34 +0100 wenzelm tuned signature;
Tue, 08 Mar 2016 14:44:11 +0100 wenzelm more abstract Session.start, without prover command-line;
Tue, 08 Mar 2016 11:18:21 +0100 wenzelm removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
Mon, 07 Mar 2016 22:40:43 +0100 wenzelm prospective command line entry point for simplified isabelle_process;
Mon, 07 Mar 2016 20:44:47 +0100 wenzelm clarified treatment of DEL;
Mon, 07 Mar 2016 18:20:22 +0100 wenzelm Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
Sun, 14 Feb 2016 13:38:31 +0100 wenzelm tuned whitespace;
Sun, 14 Feb 2016 13:23:12 +0100 wenzelm more careful quoting for the sake of Windows;
Sat, 13 Feb 2016 21:22:02 +0100 wenzelm tuned signature;
Sat, 13 Feb 2016 20:41:56 +0100 wenzelm clarified bash process -- similar to ML version;
Thu, 20 Aug 2015 20:36:06 +0200 wenzelm clarified modules, like ML version;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Tue, 12 Aug 2014 18:54:53 +0200 wenzelm tuned signature;
Tue, 12 Aug 2014 18:36:43 +0200 wenzelm generic process wrapping in Prover;
Tue, 12 Aug 2014 17:28:07 +0200 wenzelm more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
Fri, 02 May 2014 20:01:45 +0200 wenzelm prefer scala.Console with its support for thread-local redirection;
Tue, 29 Apr 2014 21:29:36 +0200 wenzelm clarified exit sequence: prover is reset afterwards, no more output messages;
Tue, 29 Apr 2014 14:50:40 +0200 wenzelm clarified;
Fri, 25 Apr 2014 12:27:18 +0200 wenzelm tuned comments;
Thu, 24 Apr 2014 16:47:47 +0200 wenzelm tuned imports;
Thu, 24 Apr 2014 15:02:13 +0200 wenzelm clarified command_input: Consumer_Thread;
Thu, 24 Apr 2014 13:54:45 +0200 wenzelm eliminated pointless output actors;
Thu, 17 Apr 2014 14:52:23 +0200 wenzelm reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
Thu, 03 Apr 2014 19:26:39 +0200 wenzelm recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
Thu, 03 Apr 2014 14:54:17 +0200 wenzelm more general prover operations;
Thu, 03 Apr 2014 13:46:18 +0200 wenzelm more general prover operations;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Sat, 16 Nov 2013 12:29:10 +0100 wenzelm more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
Fri, 15 Nov 2013 19:31:10 +0100 wenzelm more specific Protocol_Output: empty message.body, main content via bytes/text;
Thu, 14 Nov 2013 17:17:57 +0100 wenzelm tuned signature;
Tue, 01 Oct 2013 12:53:24 +0200 wenzelm tuned signature -- facilitate experimentation with other processes;
Tue, 30 Jul 2013 19:53:06 +0200 wenzelm tuned -- more uniform ML vs. Scala;
Wed, 10 Jul 2013 22:04:57 +0200 wenzelm tuned signature;
Wed, 10 Jul 2013 21:54:43 +0200 wenzelm no need for raw stdin;
Tue, 09 Apr 2013 20:34:15 +0200 wenzelm public Isabelle_Process.xml_cache (thread-safe);
Tue, 09 Apr 2013 20:27:27 +0200 wenzelm tuned signature;
Sun, 25 Nov 2012 20:17:04 +0100 wenzelm explicit module UTF8;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Sun, 18 Nov 2012 15:28:58 +0100 wenzelm update options via protocol;
Mon, 01 Oct 2012 20:17:30 +0200 wenzelm more direct message header: eliminated historic encoding via single letter;
Wed, 19 Sep 2012 17:07:25 +0200 wenzelm earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
Tue, 07 Aug 2012 12:35:24 +0200 wenzelm tuned signature -- slightly more abstract text representation of prover process;
Thu, 19 Jul 2012 20:49:17 +0200 wenzelm support for detached Bash_Job with some control operations;
Thu, 19 Jul 2012 20:02:44 +0200 wenzelm support external processes with explicit environment;
Tue, 29 May 2012 21:48:05 +0200 wenzelm clarified prover startup: no timeout, read stderr more carefully;
Tue, 29 May 2012 21:03:11 +0200 wenzelm need to close_input before expecting threads to terminate/join;
Tue, 29 May 2012 18:00:54 +0200 wenzelm more explicit treatment of return code vs. session phase;
Sat, 03 Mar 2012 18:18:39 +0100 wenzelm clarified terminology of raw protocol messages;
Sat, 03 Mar 2012 17:46:50 +0100 wenzelm tuned;
Sat, 03 Mar 2012 17:30:14 +0100 wenzelm tuned signature -- emphasize Isabelle_Process Input vs. Output;
Sat, 03 Mar 2012 11:31:12 +0100 wenzelm clarified scope of exception handlers;
Fri, 02 Mar 2012 22:34:42 +0100 wenzelm terminate after first exception -- avoid syslog flooding;
Mon, 20 Feb 2012 15:36:48 +0100 wenzelm clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
Thu, 05 Jan 2012 14:15:37 +0100 wenzelm prefer raw_message for protocol implementation;
Thu, 01 Dec 2011 14:29:14 +0100 wenzelm clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
Tue, 29 Nov 2011 20:18:02 +0100 wenzelm clarified modules;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Fri, 25 Nov 2011 18:37:14 +0100 wenzelm retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
Mon, 17 Oct 2011 11:24:22 +0200 wenzelm always use sockets on Windows/Cygwin;
Sun, 25 Sep 2011 13:48:59 +0200 wenzelm more uniform defaults;
Fri, 23 Sep 2011 13:44:31 +0200 wenzelm explicit option for socket vs. fifo communication;
Wed, 21 Sep 2011 20:35:50 +0200 wenzelm more abstract wrapping of fifos as System_Channel;
Wed, 07 Sep 2011 11:00:39 +0200 wenzelm added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
Tue, 06 Sep 2011 11:18:19 +0200 wenzelm buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
Tue, 06 Sep 2011 10:27:04 +0200 wenzelm more abstract receiver interface;
Sun, 04 Sep 2011 19:12:06 +0200 wenzelm simplified signatures;
Sun, 04 Sep 2011 14:29:15 +0200 wenzelm pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
Tue, 12 Jul 2011 19:36:46 +0200 wenzelm more uniform Properties in ML and Scala;
Mon, 11 Jul 2011 16:48:02 +0200 wenzelm JVM method invocation service via Scala layer;
Mon, 11 Jul 2011 15:56:30 +0200 wenzelm tuned signature;
Mon, 11 Jul 2011 11:13:33 +0200 wenzelm some support for raw messages, which bypass standard Symbol/YXML decoding;
Mon, 11 Jul 2011 10:27:50 +0200 wenzelm tuned XML.Cache parameters;
Sat, 09 Jul 2011 21:53:27 +0200 wenzelm echo prover input via raw_messages, for improved protocol tracing;
Thu, 07 Jul 2011 13:48:30 +0200 wenzelm simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
less more (0) -120 tip