| Sat, 14 Jan 2023 22:24:01 +0100 |
wenzelm |
proper language context;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2023 19:47:02 +0100 |
wenzelm |
more operations: use proper constants;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2023 19:16:24 +0100 |
wenzelm |
clarified types;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2023 19:07:18 +0100 |
wenzelm |
more explicit language context;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2023 17:14:59 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2023 20:09:08 +0100 |
wenzelm |
avoid confusion of markup element vs. property names;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2023 19:48:47 +0100 |
wenzelm |
clarified Latex markup: optional cite "location" consists of nested document text;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2023 16:01:49 +0100 |
wenzelm |
more explicit latex markup;
|
file |
diff |
annotate
|
| Mon, 31 Oct 2022 11:04:54 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2022 12:38:00 +0200 |
wenzelm |
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 21:02:13 +0100 |
wenzelm |
example: alternative document headings, based on more general document output markup;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2021 16:49:58 +0100 |
wenzelm |
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2021 20:42:41 +0100 |
wenzelm |
more symbolic latex_output via XML (using YXML within text);
|
file |
diff |
annotate
|
| Sat, 20 Nov 2021 18:15:09 +0100 |
wenzelm |
more symbolic latex_output via XML;
|
file |
diff |
annotate
|
| Mon, 15 Nov 2021 17:26:31 +0100 |
wenzelm |
more symbolic latex_output via XML;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 20:40:41 +0100 |
wenzelm |
more symbolic latex output;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 17:46:41 +0100 |
wenzelm |
symbolic latex_output via XML, interpreted in Isabelle/Scala;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 15:42:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 15:21:40 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2021 16:23:20 +0100 |
wenzelm |
more PIDE markup;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 22:35:44 +0200 |
wenzelm |
more markup, e.g. to locate defining theory node in formal document output;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2021 13:39:37 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
| Tue, 08 Jun 2021 13:17:45 +0200 |
wenzelm |
more formal ML profiling messages;
|
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
|
| Sat, 10 Apr 2021 21:50:59 +0200 |
wenzelm |
more robust treatment of empty markup: it allows to produce formal chunks;
|
file |
diff |
annotate
|