NEWS: more LaTeX markup

[Tobias Nipkow]

That was exactly what I needed, many thanks!

Tobias

On 13/12/2024 13:46, Makarius wrote:
> On 11/12/2024 17:25, Tobias Nipkow wrote:
>>
>> 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.
> 
> @{const [source] NAME} presents the original input source, not pretty-printed 
> output. It would require substantial reworking of the document preparation 
> system to use PIDE markup there: one happy day that will happen, but not now and 
> not for the coming release.
> 
> If this is actually about printing formal entity names like the term pretty- 
> printer does (without syntax), you can define a document antiquotation 
> @{const_name NAME} like this:
> 
> setup ‹
>    Document_Output.antiquotation_pretty_embedded \<^binding>‹const_name›
>      (Args.const {proper = true, strict = false})
>      (fn ctxt => fn c => Pretty.mark_str (Markup.const, 
> Proof_Context.extern_const ctxt c))
> ›
> 
> 
>      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/20241216/982ae0b8/attachment.bin>