| Wed, 11 Oct 2023 11:37:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 11:27:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 14:43:07 +0200 |
wenzelm |
clarified treatment of exceptions: avoid catch-all handlers;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:30:46 +0200 |
wenzelm |
clarified order of modules: early access to interrupt management of Isabelle_Threads;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 15:43:49 +0200 |
wenzelm |
proper system options to control context tracing/timing;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 16:13:08 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 22:17:11 +0200 |
wenzelm |
more scalable byte messages, notably for Scala functions in ML;
|
file |
diff |
annotate
|
| Tue, 13 Apr 2021 16:19:43 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 13 Apr 2021 11:44:47 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 22:47:55 +0200 |
wenzelm |
more uniform use of Byte_Message;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2021 12:30:52 +0100 |
wenzelm |
clarified modules: allow early definition of protocol commands;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 16:14:16 +0100 |
wenzelm |
more complete report positions, notably for command 'back' (amending eca176f773e0);
|
file |
diff |
annotate
|
| Sat, 15 Aug 2020 13:51:55 +0200 |
wenzelm |
proper protocol init (amending 065dcd80293e);
|
file |
diff |
annotate
|
| Sat, 15 Aug 2020 13:37:34 +0200 |
wenzelm |
provide protocol handlers via isabelle_system_service;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 22:57:14 +0200 |
wenzelm |
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 22:19:32 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 21:02:02 +0200 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Fri, 07 Aug 2020 20:19:49 +0200 |
wenzelm |
ML statistics via external process: allows monitoring RTS while ML program sleeps;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 22:54:22 +0200 |
wenzelm |
more thorough cleanup, e.g. before ML_Heap.save;
|
file |
diff |
annotate
|
| Sun, 24 May 2020 13:39:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
| Thu, 02 Apr 2020 20:06:43 +0200 |
wenzelm |
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
|
file |
diff |
annotate
|
| Thu, 02 Apr 2020 12:49:53 +0200 |
wenzelm |
clarified signature: more direct Isabelle_Process.EXIT;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2020 13:55:30 +0200 |
wenzelm |
traditional print_mode for batch build;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2020 12:56:19 +0200 |
wenzelm |
proper context for loading Pure;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 14:40:56 +0200 |
wenzelm |
close socket explicitly (idempotent);
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 14:09:36 +0200 |
wenzelm |
more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
|
file |
diff |
annotate
|
| Mon, 30 Mar 2020 19:39:11 +0200 |
wenzelm |
more accurate treatment of errors;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 12:39:44 +0100 |
wenzelm |
more direct output of XML material -- bypass Buffer.T;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 12:02:27 +0100 |
wenzelm |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
file |
diff |
annotate
|
| Sun, 20 Oct 2019 16:16:23 +0200 |
wenzelm |
option to export standardized proof terms (not scalable);
|
file |
diff |
annotate
|
| Wed, 02 Jan 2019 20:20:01 +0100 |
wenzelm |
more robust system channel via options that are private to the user;
|
file |
diff |
annotate
|
| Tue, 11 Dec 2018 21:23:02 +0100 |
wenzelm |
more uniform multi-language operations;
|
file |
diff |
annotate
|
| Tue, 02 Oct 2018 19:02:47 +0200 |
wenzelm |
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 11:03:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2017 13:13:25 +0200 |
wenzelm |
discontinued obsolete print mode;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 20:17:00 +0200 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
| Sat, 18 Mar 2017 13:15:07 +0100 |
wenzelm |
reset print_mode, e.g. relevant for saved heap;
|
file |
diff |
annotate
|
| Sat, 18 Mar 2017 13:06:10 +0100 |
wenzelm |
clarified init (see also 32755e357a51, ac48def96b69);
|
file |
diff |
annotate
|
| Sat, 18 Mar 2017 12:46:52 +0100 |
wenzelm |
restore output channels after shutdown, e.g. relevant for saved heap;
|
file |
diff |
annotate
|
| Sat, 18 Mar 2017 12:24:56 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2017 17:21:46 +0100 |
wenzelm |
more robust startup/init: let Session.stop wait for protocol handler initialization;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 16:16:05 +0200 |
wenzelm |
shared output primitives of physical/virtual Pure;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 14:00:23 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 17:16:30 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:51:37 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 13:41:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 12:35:11 +0100 |
wenzelm |
clarified use of options;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 17:11:30 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 20:17:37 +0100 |
wenzelm |
clarified session build options: already provided by ML_Process;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 20:33:34 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 20:24:41 +0100 |
wenzelm |
separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2015 14:01:26 +0100 |
wenzelm |
refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
|
file |
diff |
annotate
|
| Sun, 11 Jan 2015 20:40:14 +0100 |
wenzelm |
discontinued fifo channel, always use portable socket;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 20:55:11 +0100 |
wenzelm |
eliminated TTY/PG legacy;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|