NEWS: more LaTeX markup

[Tobias Nipkow]

Hi Makarius,

I am using these new macros to modify the font for constants. This works very 
well except for one issue: in latex blocks with line breaks, the \isaindent code 
does not utilize these macros but includes the bare names only. As a result, the 
indentation is a bit off. Here is an example of the generated latex code

\isaindent{{\isacharequal}{\kern0pt}\ 
{\isacharparenleft}{\kern0pt}}\isaconst{LT}\ {\isasymRightarrow}\ 
\isakeyword{let}\ \isabound{l{\isacharprime}{\kern0pt}}\ 
{\isacharequal}{\kern0pt}\ \isaconst{del}\ \isavar{x}\ \isavar{l}\isanewline
\isaindent{{\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}LT\ 
{\isasymRightarrow}\ }

\isaconst{LT} vs plain LT inside an \isaindent a few lines below.

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/20241223/54b0d8b4/attachment.bin>