NEWS: more LaTeX markup

[Tobias Nipkow]

Brilliant, many thanks!

Is there any way to obtain (in the document} \isaconst{Nil} via some antiquotation?
- @{const Nil} produces []
- @{const [source] Nil} produces \isa{Nil}

Of course this is just an example standing for the many constants that have 
associated syntax.

Tobias

On 10/12/2024 22:13, Makarius wrote:
> *** Document preparation ***
> 
> * LaTeX output from printed entities (types, terms, thms) now contains
> additional markup as follows:
> 
>    tclass    -- type class "a"
>    tconst    -- type constructor "a"
>    tfree     -- free type variable "'a"
>    tvar      -- schematic type variable "?'a"
>    const     -- constant "a"
>    free      -- free variable "a"
>    bound     -- bound variable "a"
>    skolem    -- skolem variable "a"
>    var       -- schematic variable "?a"
> 
> These markup names are turned into LaTeX macros using the prefix "\isa",
> e.g. "\isaconst{...}" for "const". By default, these macros have no
> effect, but may be defined in root.tex like this:
> 
>    \renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
>    \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
> 
> 
> This refers to Isabelle/f8b28356ab94.
> 
> It has required many decades to get to that point: I now recallthat in the late 
> 1990ies, we could only get free/bound/var etc. but not the consts. Thanks to 
> major cleanup of the inner-syntax framework some months ago, this now turned out 
> reasonably easy.
> 
> 
>      Makarius

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5187 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241211/c3a4deaf/attachment.bin>