| 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
|
| Mon, 07 Aug 2017 15:13:21 +0200 |
wenzelm |
more synchronized Execution.snapshot;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:34:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 14:09:03 +0200 |
wenzelm |
eliminated default_qualifier: just a constant;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:43:21 +0200 |
wenzelm |
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 13:19:24 +0200 |
wenzelm |
proper qualifier for imports;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 11:52:21 +0200 |
wenzelm |
clarified, according to Scala version;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 11:29:47 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 22:36:32 +0200 |
wenzelm |
more qualifier treatment, but in the end it is still ignored;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 21:35:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 21:28:19 +0200 |
wenzelm |
provide Resources.import_name in ML, similar to Scala version;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 16:29:52 +0100 |
wenzelm |
absent timing information means zero, according to 0070053570c4, f235646b1b73;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 19:07:16 +0100 |
wenzelm |
consolidate nested thms with persistent result, for improved performance;
|
file |
diff |
annotate
|
| Sun, 10 Apr 2016 20:15:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|