| 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
|
| Wed, 26 Nov 2014 15:44:32 +0100 |
wenzelm |
even more exception traces for Document.update, which goes through additional execution wrappers;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 14:35:55 +0100 |
wenzelm |
more informative failure of protocol commands, with exception trace;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 17:08:54 +0100 |
wenzelm |
eliminated odd flags and hook;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:19:04 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2014 13:39:59 +0200 |
wenzelm |
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 18:36:43 +0200 |
wenzelm |
generic process wrapping in Prover;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 16:10:59 +0200 |
wenzelm |
more frugal standard message properties;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:59:15 +0200 |
wenzelm |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 12:00:17 +0100 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:39:04 +0100 |
wenzelm |
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 17:58:03 +0100 |
wenzelm |
merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
|
file |
diff |
annotate
|
| Thu, 28 Nov 2013 12:54:39 +0100 |
wenzelm |
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 22:10:45 +0100 |
wenzelm |
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
|
file |
diff |
annotate
|
| Mon, 11 Nov 2013 20:00:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|