| Thu, 12 Sep 2024 14:24:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:13:59 +0200 |
wenzelm |
clarified print_mode (again, amending 9de19e3a7231): support e.g. 'thm ("") symmetric' for formatting in ML and without markup;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:10:36 +0200 |
wenzelm |
more robust reports: ensure that markup is actually present;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:09:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 11 Sep 2024 23:26:25 +0200 |
wenzelm |
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
|
changeset |
files
|
| Wed, 11 Sep 2024 23:07:18 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 11 Sep 2024 22:56:42 +0200 |
wenzelm |
misc tuning and clarification (see also 86a31308a8e1);
|
changeset |
files
|
| Wed, 11 Sep 2024 22:28:42 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Wed, 11 Sep 2024 21:41:33 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 21:25:15 +0200 |
wenzelm |
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
|
changeset |
files
|
| Wed, 11 Sep 2024 20:45:17 +0200 |
wenzelm |
clarified YXML bootstrap;
|
changeset |
files
|
| Wed, 11 Sep 2024 20:06:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 11 Sep 2024 20:05:09 +0200 |
wenzelm |
more robust: global ML name space for markup elements;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:59:10 +0200 |
wenzelm |
clarified properties;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:53:35 +0200 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:35:21 +0200 |
wenzelm |
further clarification of print_mode: PIDE markup depends on "isabelle_process" alone, Latex is stateless;
|
changeset |
files
|
| Wed, 11 Sep 2024 17:00:02 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 11 Sep 2024 15:36:14 +0200 |
wenzelm |
minor performance tuning, notably for Bytes.add (e.g. YXML output);
|
changeset |
files
|
| Wed, 11 Sep 2024 12:46:56 +0200 |
wenzelm |
revert 90f6e541e926, which has become pointless thanks to df85df6315af;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:32:11 +0200 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:18:29 +0200 |
wenzelm |
clarified files;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:11:47 +0200 |
wenzelm |
drop pointless print_mode operations Output.output / Output.escape;
|
changeset |
files
|
| Tue, 10 Sep 2024 20:36:01 +0200 |
wenzelm |
clarified signature: prefer explicit type Bytes.T;
|
changeset |
files
|
| Tue, 10 Sep 2024 20:06:51 +0200 |
wenzelm |
clarified signature, roughly following Isabelle/Scala;
|
changeset |
files
|
| Tue, 10 Sep 2024 19:57:45 +0200 |
wenzelm |
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
|
changeset |
files
|
| Tue, 10 Sep 2024 16:06:38 +0200 |
wenzelm |
tuned comments, following Isabelle/ML;
|
changeset |
files
|
| Tue, 10 Sep 2024 16:03:42 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Tue, 10 Sep 2024 15:35:51 +0200 |
wenzelm |
tuned;
|
changeset |
files
|