src/Pure/Thy/document_output.ML
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Sun, 05 Dec 2021 16:26:03 +0100 wenzelm prefer symbolic Latex.environment (typeset in Isabelle/Scala);
Wed, 24 Nov 2021 15:33:43 +0100 wenzelm more uniform treatment of optional_argument for Latex elements;
Tue, 23 Nov 2021 20:46:40 +0100 wenzelm more general document output: enclosing markup is defined in user-space;
Tue, 23 Nov 2021 16:06:09 +0100 wenzelm output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
Tue, 23 Nov 2021 12:29:09 +0100 wenzelm clarified modules;
Mon, 22 Nov 2021 16:49:58 +0100 wenzelm source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
Sat, 20 Nov 2021 20:42:41 +0100 wenzelm more symbolic latex_output via XML (using YXML within text);
Sat, 20 Nov 2021 18:15:09 +0100 wenzelm more symbolic latex_output via XML;
Mon, 15 Nov 2021 17:26:31 +0100 wenzelm more symbolic latex_output via XML;
Mon, 15 Nov 2021 11:38:14 +0100 wenzelm clarified signature;
Sat, 13 Nov 2021 17:22:10 +0100 wenzelm tuned whitespace;
Tue, 28 Sep 2021 16:01:13 +0200 wenzelm outer syntax: support for control-cartouche tokens;
Tue, 25 May 2021 22:28:39 +0200 wenzelm compose Latex text as XML, output exported YXML in Isabelle/Scala;
Fri, 21 May 2021 12:29:29 +0200 wenzelm clarified modules;
less more (0) tip