| Sun, 06 Jun 2021 14:12:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 22:01:16 +0200 |
wenzelm |
tuned --- avoid redundant future tasks from already loaded theories;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 21:46:14 +0200 |
wenzelm |
no comment --- topological order appears to be fine since 04-Mar-2013;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 21:36:42 +0200 |
wenzelm |
more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7);
|
file |
diff |
annotate
|
| Tue, 25 May 2021 23:37:32 +0200 |
wenzelm |
clarified document export names;
|
file |
diff |
annotate
|
| Tue, 25 May 2021 22:28:39 +0200 |
wenzelm |
compose Latex text as XML, output exported YXML in Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
|
| Wed, 12 May 2021 16:47:52 +0200 |
wenzelm |
clarified signature: provide access to previous state;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 22:47:55 +0200 |
wenzelm |
more uniform use of Byte_Message;
|
file |
diff |
annotate
|
| Mon, 04 Jan 2021 19:56:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Jan 2021 19:28:50 +0100 |
wenzelm |
proper thread position for reports;
|
file |
diff |
annotate
|
| Mon, 04 Jan 2021 14:23:43 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2020 22:07:14 +0100 |
wenzelm |
clarified protocol: support "isabelle log" on failed theories as well;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 21:08:43 +0100 |
wenzelm |
recovered document output from 6bc199a70bf9;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 17:49:09 +0100 |
wenzelm |
more robust: include reports from Thy_Output.present_thy/output_document;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 13:30:06 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 15:14:58 +0100 |
wenzelm |
support for PIDE markup in batch build (inactive due to pide_reports=false);
|
file |
diff |
annotate
|
| Fri, 20 Nov 2020 23:47:34 +0100 |
wenzelm |
generate theory HTML in Isabelle/Scala;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2020 15:47:53 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2020 22:57:56 +0100 |
wenzelm |
refer to command_timings/last_timing via resources;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:46:02 +0100 |
wenzelm |
clarified signature: master_dir is just Path.current;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:23:04 +0100 |
wenzelm |
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
|
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 17:34:19 +0100 |
wenzelm |
clarified bibtex_entries: refer to overall session structure;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2020 17:29:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 21:00:14 +0100 |
wenzelm |
build documents in Isabelle/Scala, based on generated tex files as session exports;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Sat, 26 Sep 2020 16:02:54 +0200 |
wenzelm |
clarified document export;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2020 18:03:17 +0200 |
wenzelm |
discontinue export_document --- always enabled (reverting f0f83ce0badd);
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 15:53:09 +0100 |
wenzelm |
clarified signature;
|
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 15:30:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2019 20:54:47 +0100 |
wenzelm |
clarified signature: more explicit type Path.binding;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 19:22:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 02 Feb 2019 15:52:14 +0100 |
wenzelm |
clarified signature: Path.T as in Generated_Files;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2018 11:44:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:39:49 +0200 |
wenzelm |
prefer explicit options;
|
file |
diff |
annotate
|
| Sun, 24 Jun 2018 22:13:23 +0200 |
wenzelm |
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 22:22:47 +0200 |
wenzelm |
support for dynamic document output while editing;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 16:00:10 +0200 |
wenzelm |
tuned signature (see Command.eval_state);
|
file |
diff |
annotate
|
| Mon, 14 May 2018 14:30:13 +0200 |
wenzelm |
export generated document.tex, unless explicit document=false;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 11:29:22 +0200 |
wenzelm |
more general presentation hook, with document preparation as application;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 10:58:14 +0200 |
wenzelm |
clarified signature: more explicit type "context" with full options;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 10:22:45 +0200 |
wenzelm |
more explicit type Thy_Output.segment;
|
file |
diff |
annotate
|
| Fri, 11 May 2018 22:40:02 +0200 |
wenzelm |
support for general theory presentation;
|
file |
diff |
annotate
|
| Wed, 09 May 2018 20:45:57 +0200 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 17:40:57 +0100 |
wenzelm |
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2017 16:18:40 +0100 |
wenzelm |
positions as postlude: avoid intrusion of odd %-forms into main tex source;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2017 14:29:14 +0100 |
wenzelm |
more explicit latex errors;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2017 16:02:44 +0100 |
wenzelm |
removed somewhat pointless warning;
|
file |
diff |
annotate
|
| Mon, 16 Oct 2017 14:32:09 +0200 |
wenzelm |
provide theory timing information, similar to command timing but always considered relevant;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2017 11:53:55 +0200 |
wenzelm |
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 11:49:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 20:05:23 +0200 |
wenzelm |
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
|
file |
diff |
annotate
|