| 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
|
| Tue, 28 Jun 2022 14:50:59 +0200 |
wenzelm |
more operations on Bytes.T;
|
file |
diff |
annotate
|
| Tue, 28 Jun 2022 11:24:59 +0200 |
wenzelm |
more operations on Bytes.T;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2021 14:26:13 +0100 |
wenzelm |
more PIDE markup;
|
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
|
| Fri, 18 Dec 2020 23:19:07 +0100 |
wenzelm |
improved markup for theory header imports;
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 21:59:23 +0100 |
wenzelm |
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2020 22:05:59 +0100 |
wenzelm |
more uniform Resources.init_session via YXML;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 13:11:15 +0100 |
wenzelm |
refer to HTML symbols via resources;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 22:00:45 +0100 |
wenzelm |
refer to session structure from resources;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 17:34:19 +0100 |
wenzelm |
clarified bibtex_entries: refer to overall session structure;
|
file |
diff |
annotate
|
| Sun, 27 Sep 2020 17:02:59 +0200 |
wenzelm |
ISABELLE_PDFLATEX is now lualatex;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 17:05:59 +0200 |
wenzelm |
strict init of protocol handlers;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2020 13:13:29 +0200 |
wenzelm |
clarified GUI;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 22:43:40 +0200 |
wenzelm |
discontinued old batch-build functionality;
|
file |
diff |
annotate
|
| Sun, 24 May 2020 14:15:44 +0200 |
wenzelm |
clarified build_session protocol;
|
file |
diff |
annotate
|
| Sun, 24 May 2020 12:38:41 +0200 |
wenzelm |
more robust: explicit check for PIDE session;
|
file |
diff |
annotate
|
| Sun, 24 May 2020 10:36:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 20:24:52 +0100 |
wenzelm |
proper message (amending 94442fce40a5);
|
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
|
| Mon, 16 Sep 2019 16:00:10 +0200 |
wenzelm |
find theories via session directories only -- ignore known_theories;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 13:33:09 +0200 |
wenzelm |
find theory files via session structure: much faster Prover IDE startup;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 19:44:54 +0200 |
wenzelm |
prefer commands_accepted: fewer protocol messages;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 18:59:24 +0200 |
wenzelm |
prefer define_commands_bulk: fewer protocol messages;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 17:10:23 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 19 May 2019 18:10:45 +0200 |
wenzelm |
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2019 21:37:24 +0100 |
wenzelm |
more scalable on 32-bit Poly/ML;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2019 21:30:16 +0100 |
wenzelm |
more compact representation: approx. factor 2;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2019 17:33:39 +0100 |
wenzelm |
more scalable on 32-bit Poly/ML;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2018 16:12:26 +0200 |
wenzelm |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
file |
diff |
annotate
|
| Thu, 31 May 2018 22:27:13 +0200 |
wenzelm |
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
|
file |
diff |
annotate
|
| Tue, 23 Jan 2018 19:25:39 +0100 |
wenzelm |
treat sessions as entities with defining position;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2018 14:55:46 +0100 |
wenzelm |
formal treatment of documentation names;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 21:53:07 +0100 |
wenzelm |
added document antiquotation @{session name};
|
file |
diff |
annotate
|
| Thu, 28 Sep 2017 15:11:32 +0200 |
wenzelm |
session-qualified theory names are mandatory;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 22:13:05 +0200 |
wenzelm |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 15:13:21 +0200 |
wenzelm |
more synchronized Execution.snapshot;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 14:09:03 +0200 |
wenzelm |
eliminated default_qualifier: just a constant;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2017 12:39:36 +0200 |
wenzelm |
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 21:13:43 +0200 |
wenzelm |
global session_base for PIDE interaction;
|
file |
diff |
annotate
|
| Sat, 18 Mar 2017 12:24:56 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2016 11:18:35 +0200 |
wenzelm |
tuned signature: more uniform Keyword.spec;
|
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: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
|
| Mon, 29 Feb 2016 15:23:13 +0100 |
wenzelm |
clarified ML heap operations;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 16:21:34 +0200 |
wenzelm |
more explicit HTML.symbols;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 19:25:13 +0200 |
wenzelm |
output HTML text according to Isabelle/Scala Symbol.Interpretation;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 20:55:46 +0200 |
wenzelm |
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 13:55:01 +0200 |
wenzelm |
GUI controls for ML_statistics, for more digestible protocol dump;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 16:00:19 +0200 |
wenzelm |
more position information and PIDE markup for command keywords;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:30:54 +0100 |
wenzelm |
tuned protocol -- resolve command positions in ML;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 22:00:51 +0100 |
wenzelm |
clarified markup for embedded files, early before execution;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:12:30 +0100 |
wenzelm |
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2015 22:19:22 +0100 |
wenzelm |
more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);
|
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
|